We present $\lambda_{\mathsf{ert}}$, a type theory supporting refinement types with <em>explicit proofs</em>. 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.
Thu 7 SepDisplayed time zone: Pacific Time (US & Canada) change
Thu 7 Sep
Displayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | Verification 2ICFP Papers and Events at B - Fifth Avenue Chair(s): Niki Vazou IMDEA Software Institute | ||
10:30 30mTalk | Explicit Refinement Types ICFP Papers and Events DOI | ||
11:00 30mTalk | Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)Experience Report ICFP Papers and Events Thomas Bourgeat , Ian Clester Georgia Institute of Technology, Andres Erbsen MIT, Samuel Gruetter Massachusetts Institute of Technology, Pratap Singh CMU, Andy Wright MIT, Adam Chlipala Massachusetts Institute of Technology DOI |