Type-directed Program Synthesis
Program synthesis is the process by which we derive programs automatically from specification. Traditionally a pursuit of the formal methods community, program synthesis has strong ties with type-directed programming, type checking, and type inference. We are building type-theoretic foundations for program synthesis as well as exploring the application of these techniques to richly-typed functional programming languages.
- Kevin Connors (Grinnell College)
- Jonathan Frankle (Princeton University)
- Reilly Grant (Grinnell College)
- Anders Miltner (Princeton University)
- Peter-Michael Osera (Grinnell College)
- Zachary Segall (Grinnell College)
- Rohan Shah (University of Pennsylvania)
- David Walker (Princeton University)
- Steve Zdancewic (University of Pennsylvania)
Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic.
Example-Directed Synthesis: A Type-Theoretic Interpretation [pdf, github].
In Principles of Programming Languages (POPL), January 2016.
Program Synthesis with Types [pdf, github].
PhD thesis. University of Pennsylvania. 2015.
Peter-Michael Osera and Steve Zdancewic.
Type-and-example-directed Program Synthesis [pdf, github].
In Programming Language Design and Implementation (PLDI), June 2015.
This work is supported in part by the NSF under awards CCF-1138996 and CNS-1111520.