Correct-by-Construction eta-conversion for Agda Core
A. de Vries (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Z. Erkin – Graduation committee member (TU Delft - Electrical Engineering, Mathematics and Computer Science)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Software correctness is a hard problem. Dependently-typed programming languages like Agda help us to provide guarantees about software while writing it in a Correct-by-Construction (CbC) manner. However, the implementation of a dependently-typed programming language may contain bugs itself: Agda has bugs in its own implementation on a regular basis. Dependently typed-typed programming languages should therefore verify themselves in a Correct-by-Construction manner using their own components: self-verification. Agda Core aims to do this for Agda: it is a core language for Agda and provides a Correct-by-Construction type checker for itself derived from a trusted type theory, written in Agda.
Before Agda Core can be used as a true self-verifier for Agda and be integrated into Agda’s main compiler and type checker, more features from Agda need to be supported by it. In this thesis, we focus on Agda’s η-conversion for function types and record types. We formalize η-conversion for function types and record types with at least one field using untyped conversion: we also add support for records to Agda Core along the way. We also show progress towards a formalization of Agda’s η-conversion using typed conversion, which allows for formalizing the often tricky-considered η-conversion for Agda’s unit type. For all of these formalizations, we show that they can be added to Agda Core with reasonable effort. Overall, this work therefore provides an important step towards the ultimate goal of a self-verified type checker for Agda with support for all of Agda’s features, which decreases the future potential for bugs in Agda’s implementation with relation to η-conversion, and teaches us how to self-verify η-conversion for a dependently-typed language.