Explicit Refinement Types

• Published in: Proceedings of the ACM on Programming Languages
• Main Authors: Ghalayini, Jad Elkhaleq, Krishnaswami, Neel
• Other Authors: European Research Commission
• Format: Article in Journal/Newspaper
• Language: English
• Published: Association for Computing Machinery (ACM) 2023
• Subjects: DML
• Online Access: http://dx.doi.org/10.1145/3607837; https://dl.acm.org/doi/pdf/10.1145/3607837

We present λ ert , a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties within the program text, letting us support a rich logic of properties including quantifiers and induction. We show that the type system is sound by showing that every refined program erases to a simply-typed program, and by means of a denotational semantics, we show that every erased program has all of the properties demanded by its refined type. All of our proofs are formalised in Lean 4.