UC San Diego

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 λ_RF, 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. 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 LiquidHaskell's refinement types can be used for mechanization. Second, we mechanize our results in Coq, which comes with stronger soundness guarantees than LiquidHaskell, thereby laying the foundations for mechanizing the metatheory of LiquidHaskell. Finally, we present an extension λ_RFD, which adds lists and a length measure. We extend the metatheory to prove the soundness of the extended type system and give another mechanization in Coq.