Mechanizing Refinement Types

Explore a 20-minute video presentation from the POPL 2024 conference that delves into the mechanization of refinement types. Learn about λRF, a core refinement calculus combining semantic subtyping and parametric polymorphism. Discover how the researchers developed a metatheory for this calculus and proved the soundness of the type system. Gain insights into two mechanization approaches: the novel use of data propositions in LiquidHaskell and a Coq implementation for stronger soundness guarantees. Understand the implications for formalizing the metatheory of practical refinement type checkers and their applications in program verification.

[POPL'24] Mechanizing Refinement Types