Mechanizing Refinement Types (extended)

TL;DR

This paper introduces mbda_RF, a core refinement calculus combining semantic sub-typing and parametric polymorphism, with a formal meta-theory and mechanization using LiquidHaskell to verify sophisticated program properties.

Contribution

It provides the first formal meta-theoretic framework for refinement type systems combining semantic sub-typing and polymorphism, along with a mechanized proof in LiquidHaskell.

Findings

Meta-theory for mbda_RF established and proven sound.

Mechanization of the meta-theory using LiquidHaskell demonstrated.

Formal foundation for refinement type systems with combined features.

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.