Explicit Refinement Types ...

• Main Authors: Ghalayini, Jad Elkhaleq, Krishnaswami, Neel
• Format: Text
• Language: unknown
• Published: arXiv 2023
• Subjects: Programming Languages cs.PL; FOS Computer and information sciences; D.3.1; D.3.4; F.3.2; F.3.1; DML
• Online Access: https://dx.doi.org/10.48550/arxiv.2311.13995; https://arxiv.org/abs/2311.13995

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. ... : 31 pages, published at ICFP 2023 ...