Explicit Refinement Types
summary
System called λert implements refinement types that require explicit, checkable proofs instead of SMT solving, supporting quantifiers and induction; key claim is that every refined program erases to a simply-typed program and every erased program satisfies its refinements by a denotational semantics. Implementation and metatheory are formalized as 15,000 lines of Lean 4, with proofs of soundness and consistency, ghost variables erased at runtime, and examples showing typical proofs (e.g. length preservation, arithmetic lemmas) written and checked.
AI-written summary · about
chapters (14)
- 0:00Introduction to the problem
- 1:02Refinement types vs Agda
- 1:41Dependent types in Agda
- 2:33Challenges with equality
- 3:21Refinement types implementation
- 3:54Automation and trade-offs
- 5:39Proposed research goal
- 6:35Proof structure and erasing
- 8:26Comparing proof methodologies
- 10:16Type system and semantics
- 12:17Formal judgments and semantics
- 13:45System properties and consistency
- 16:54Conclusion and recap
- 17:55Q&A session
related talks
46mRefinement Types from Light to Deep Verification
16mA Hoare-Logic Style Refinement Types Formalisation
34mLiquid Haskell: Verification with Refinement Types
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
21mRefinement Type Refutations
35mThe Mastermind behind Refinement Types
30mTrustworthy Formal Natural Language Specifications
01h 04mLean4Lean: Mechanizing the Metatheory of Lean