November 1, 2024
A refinement type system allows programmers to express precise properties of their code with type annotations; these properties can then be verified automatically by the typechecker. 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 previously proved elusive. This thesis presents $\lambda_{RF}$, a core refinement calculus that combines semantic subtyping and parametric polymorphism. In this talk, I will develop a metatheory for this calculus and prove the soundness of the type system. Next, I will introduce data propositions, a novel feature that enables encoding derivation trees for inductively defined judgments as refined data types, and use them to show how LiquidHaskell’s refinement types can be used for mechanization. Finally, I present two mechanizations of the metatheory. Together these contributions lay the foundations for mechanizing the metatheory of LiquidHaskell.
About Michael Borkowski
Michael Borkowski is an Assistant Professor of Practice in the Department of Computer Science at Purdue University. He earned his PhD this year from the Department of Computer Science and Engineering (CSE) at the University of California, San Diego. He research interests are in software verification, type theory, and interactive theorem provers. Michael is interested in developing software verification techniques to make correct and performant software systems easier to write and understand, as well as having stronger theoretical soundness guarantees.