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 $\lambda_{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. 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 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.
Fri 19 JanDisplayed time zone: London change
15:10 - 16:30 | |||
15:10 20mTalk | Mechanizing Refinement Types POPL Michael Borkowski University of California, San Diego, Niki Vazou IMDEA Software Institute, Ranjit Jhala University of California at San Diego | ||
15:30 20mTalk | VST-A: A Foundationally Sound Annotation Verifier POPL Litao Zhou Shanghai Jiao Tong University; University of Hong Kong, Jianxing Qin Shanghai Jiao Tong University, Qinshi Wang Princeton University, Andrew W. Appel Princeton University, Qinxiang Cao Shanghai Jiao Tong University | ||
15:50 20mTalk | Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules POPL Ling Zhang Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Jinhua Wu Shanghai Jiao Tong University, Jérémie Koenig Yale University, Zhong Shao Yale University Pre-print | ||
16:10 20mTalk | A Formalization of Core Why3 in Coq POPL | ||