Generic Bidirectional Typing in a Logical Framework for Dependent Type Theories
Wednesday 18 September 2024, at 15h
ENS Paris-Saclay, room 1Z18, Zoom link
The current version of the manuscript can be found here.
Abstract.
Dependent type theories are formal systems that can be used both as programming languages and for the formalization of mathematics, and constitute the foundation of popular proof assistants such as Coq and Agda. In order to unify their study, Logical Frameworks (LFs) provide a unified meta-language for defining such theories in which various universal notions are built in by default and metatheorems can be proven in a theory-independent way.
This thesis focuses on LFs designed with implementation in mind, with the goal of providing generic type-checkers. Our main contribution is a new such LF which allows for representing type theories with their usual non-annotated syntaxes. The key to allowing the removal of annotations without jeopardizing decidability of typing is the integration of bidirectional typing, a discipline in which the typing judgment is decomposed into inference and checking modes. While bidirectional typing has been well known in the literature for quite some time, one of the central contributions of our work is that, by formulating it in an LF, we give it a generic treatment for all theories fitting our framework. Our proposal has been implemented in the generic type-checker BiTTs, allowing it to be used in practice with various theories.
In addition to our main contribution, we also advance the study of Dedukti, a sibling LF of our proposed framework. First, we revisit the problem of showing that theories are correctly represented in Dedukti by proposing a methodology for encodings which allows for showing their conservativity easily. Furthermore, we demonstrate how Dedukti can be used in practice as a tool for translating proofs by proposing a transformation for sharing proofs with predicative systems. This transformation has allowed for the translation of proofs from Matita to Agda, yielding the first-ever Agda proofs of Fermat's Little Theorem and Bertrand's Postulate.
Members of the jury:
- Andrej Bauer, University of Ljubljana - Reviewer
- Herman Geuvers, Radboud University Nijmegen - Reviewer
- Marc Bezem, University of Bergen
- Christine Paulin-Mohring, Université Paris-Saclay
- Temur Kutsia, Johannes Kepler University Linz
- Frank Pfenning, Carnegie Mellon University
- Frédéric Blanqui, Inria Saclay - Supervisor
- Gilles Dowek, Inria Saclay & ENS Paris-Saclay - Supervisor