Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language
Dependently typed languages allow us to state a program’s expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just software, so can we really trust them? The goal of this paper is to develop a lightweight technique to improve their trustworthiness by giving a formal specification of the typing rules and intrinsically verifying the typechecker with respect to these rules. Concretely, we apply this technique to a subset of Agda’s internal language, implemented in Agda. Our development relies on erasure annotations to separate the specification from the runtime of the typechecker. We provide guidelines for making design decisions for certified core typecheckers and evaluate trade-offs.
Wed 23 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
10:30 - 12:00 | Type theory and Semantic Frameworks IIResearch Papers at Yamauchi Hall Chair(s): Pierre-Evariste Dagand IRIF / CNRS | ||
10:30 30mTalk | Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language Research Papers | ||
11:00 30mTalk | Extending the Quantitative Pattern-Matching Paradigm Research Papers Sandra Alves University of Porto, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France, Miguel Ramos Universidade do Porto, LIACC; Université Paris Cité, IRIF, CNRS | ||
11:30 30mTalk | On Computational Indistinguishability and Logical Relations Research Papers Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Zeinab Galal University of Bologna, Giulia Giusti ENS Lyon |