Refinement Types for Program Verification and Synthesis
In this tutorial you will learn how refinement types—types decorated with decidable predicates—can be used for automated SMT-based program analysis and synthesis. The presentation will focus on two programming tools we have developed. The first one is LiquidHaskell, a program verifier that relies on refinement type inference to analyze advanced language features like higher order functions, polymorphism, and algebraic data types, leading to practical verification of real-world Haskell code, including safe pointer arithmetic, array indexing and functional correctness of AVL/Red-Black trees. The second tool is Synquid, a program synthesizer that generates recursive functional programs that provably satisfy a given specification in the form of a refinement type. The tutorial will include hands-on exercises, so bring your laptops!