Explore type-driven program synthesis and its applications in improving software quality through this conference talk. Delve into the use of declarative constructs and program synthesis technology to translate specifications into executable code. Learn about refinement type checking as a verification mechanism that combines types and SMT solving for automatic reasoning. Discover two applications: Synquid, a tool for creating recursive functional programs from refinement types, and Lifty, a language that uses type-driven synthesis to repair information flow leaks. Examine case studies involving complex data structures, information flow policies, and automated access check insertion. Gain insights into the future of programming, including orthogonal concerns, information security, and resource-aware programming through synthesis-aided techniques.
Overview
Syllabus
Intro
my goal: automate programming
example: insert into a sorted list
insert in a functional language
specification for insert
program synthesis
types are specifications
refinement types: sorted lists
insert in Synquid
case study: negation normal form
nnf: data types
nnf: specification
nnf: synthesized code
the future of programming (not)
orthogonal concerns
information leaks
information security with Lifty
timing attacks
resource-aware programming with ReSyn
synthesis-aided programming
Taught by
Strange Loop Conference
