ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Thu 7 Sep 2023 10:30 - 11:00 at B - Fifth Avenue - Verification 2 Chair(s): Niki Vazou

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 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
30m
Talk
Explicit Refinement Types
ICFP Papers and Events
Jad Elkhaleq Ghalayini University of Cambridge, Neel Krishnaswami University of Cambridge
DOI
11:00
30m
Talk
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