Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language

Abstract

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 type checker 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 type checker. We provide guidelines for making design decisions for certified core type checkers and evaluate trade-offs.