Program Synthesis from Refinement Types

Опубликовано 22 июня 2016, 2:45

The key to scalable program synthesis is modular verification, which enables pruning inviable candidates for each component of the target program independently. In this talk I will present Synquid: a synthesizer that takes advantage of the modularity offered by refinement type checking to efficiently generate recursive functional programs that satisfy a given specification in the form of a refinement type. The use of parametric polymorphism, coupled with automatic instantiation via Liquid Types inference, significantly enhances the expressive power of the system, allowing Synquid to synthesize programs that require elaborate reasoning from concise specifications.