Mechanizing Refinement Types (extended)
Abstrak
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 λ_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.
Topik & Kata Kunci
Penulis (3)
Michael Borkowski
Niki Vazou
Ranjit Jhala
Akses Cepat
- Tahun Terbit
- 2022
- Bahasa
- en
- Sumber Database
- arXiv
- Akses
- Open Access ✓