Type-Driven Program Synthesis

Опубликовано 26 августа 2016, 0:19

A promising approach to improving software quality is to enhance programming languages with declarative constructs, such as logical specifications or examples of desired behavior, and to use program synthesis technology to translate these constructs into efficiently executable code. In order to produce code that provably satisfies a rich specification, the synthesizer needs to be equipped with an advanced program verification mechanism that is sufficiently expressive, automatic, and modular. In this work we propose a program synthesis technique based on refinement type checking: a verification mechanism that supports automatic reasoning about expressive properties through a combination of an ML-style type system and SMT-decidable theories. The talk will present two applications of such type-driven synthesis. The first one is a program synthesizer called Synquid, which creates recursive functional programs from scratch given a refinement type as input. Synquid is the first synthesizer to automatically discover provably correct implementations of sorting algorithms, as well as balancing and insertion operations on Red-Black Trees and AVL Trees. The second application is a language called Lifty, which uses type-driven synthesis to repair information flow leaks. In Lifty, the programmer can specify expressive information flow policies by annotating the sources of sensitive data with refinement types, and the compiler automatically inserts access checks necessary to enforce these policies across the code.