Mechanizing Refinement Types (extended)
Abstract
Practical checkers based on refinement types use the combination of implicit semantic sub-typing and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal meta-theoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present \lambda_RF a core refinement calculus that combines semantic sub-typing and parametric polymorphism. We develop a meta-theory for this calculus and prove soundness of the type system. Finally, we give a full mechanization of our meta-theory using the refinement-type based LiquidHaskell as a proof checker, showing how refinements can be used for mechanization.
Cite
@article{arxiv.2207.05617,
title = {Mechanizing Refinement Types (extended)},
author = {Michael Borkowski and Niki Vazou and Ranjit Jhala},
journal= {arXiv preprint arXiv:2207.05617},
year = {2022}
}
Comments
32 pages, under review