Practical checkers based on refinement types use the combination of implicit semantic subtyping and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal metatheoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present λ R F , a core refinement calculus that combines semantic subtyping and parametric polymorphism. We develop a metatheory for this calculus and prove soundness of the type system. Finally, we give two mechanizations of our metatheory. First, we introduce data propositions , a novel feature that enables encoding derivation trees for inductively defined judgments as refined data types, and use them to show that L iquid H askell ’s refinement types can be used for mechanization. Second, we mechanize our results in C oq , which comes with stronger soundness guarantees than L iquid H askell , thereby laying the foundations for mechanizing the metatheory of L iquid H askell .

@article{paperbot2660,
  title = {Mechanizing Refinement Types},
  author = {Michael H. Borkowski and Niki Vazou and Ranjit Jhala},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632912}
}