Foundations of Type Theory for Computation and Mathematics
Abstract
Our research group worked on topics in foundations of type theory, homotopy type theory, and theory of programming languages. This abstract provides an overview of our research for the entire duration of the project. Please refer to the attached document for a more detailed description of our work, lists of external collaborators and publications, and summary of other scientific activities by our research group. Foundations of type theory. We developed a comprehensive meta-theory of general type theories. We gave a precise definition of what type theories are and identified properties that a type theory must have in order to be well-behaved. These results provide a frame-work within which type theories may be systematically studied, developed, and designed. Large parts of the development were formalized in the Coq proof assistant. We also developed a generic proof assistants, Andromeda 2, which implements (the finitary variant of) general type theories. The proof assistant allows the user to specify any standard type theory, and is equipped with a general user-extensible equality checker. We used the techniques from programming language design, namely algebraic effects and handlers, to allow the user to easily extend the proof assistant with custom proof development techniques
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 02, 2021
- Accession Number
- AD1154815
Entities
People
- Andrej Bauer
Organizations
- University of Ljubljana