Mechanizing Refinement Types

on YouTube ↗20m

" summary

Introduces λRF, a core calculus that actually combines semantic subtyping with parametric polymorphism and proves soundness; develops two mechanizations: one in LiquidHaskell (adds a positivity checker and uses the equations library workaround) and one in Coq (full denotational mechanization); introduces data propositions to encode derivation trees; proves standard type safety and denotational soundness; artifacts and proofs are available and the LiquidHaskell path required a concrete patch to avoid unsoundness.

AI-written summary · about

" chapters (11)

1. 0:00Refinement types intro
2. 1:05Challenges in refinement types
3. 3:11Arrays as functions example
4. 7:59Circularity in subtyping
5. 9:50Stratifying the calculus
6. 10:53Refinement implication formalized
7. 11:35Polymorphism with refinements
8. 13:21Type safety mechanized
9. 14:45Lessons from LiquidHaskell
10. 15:29Conclusion and future
11. 15:50Q&A