Finitary type theories with and without contexts

Haselwarter, Philipp Georg (author), Bauer, Andrej (author)

We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin–Löf type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presuppositions, uniqueness of typing, and inversion principles. We then give a second formulation of finitary type theories in which there are no explicit contexts. Instead, free variables are explicitly annotated with their types. We provide translations between finitary type theories with and without contexts, thereby showing that they have the same expressive power. The context-free type theory is implemented in the nucleus of the Andromeda 2 proof assistant.

• Language: English
• Keywords: dependent type theory, context-free type theory, formal meta-theory, proof assistants
• Work type: Article
• Typology: 1.01 - Original Scientific Article
• Organization: FMF - Faculty of Mathematics and Physics
• Publication status: Published
• Publication version: Version of Record
• Year: 2023
• Number of pages: 87 str.
• Numbering: Vol. 67, iss. 4, art. 36
• PID: 20.500.12556/RUL-152580
• UDC: 510.6
• ISSN on article: 0168-7433
• DOI: 10.1007/s10817-023-09678-y
• COBISS.SI-ID: 168229379
• Publication date in RUL: 29.11.2023

Record is a part of a journal

• Title: Journal of automated reasoning
• Shortened title: J. autom. reason.
• Publisher: Springer Nature
• ISSN: 0168-7433
• COBISS.SI-ID: 25709824

Licences

• License: CC BY 4.0, Creative Commons Attribution 4.0 International
• Link: http://creativecommons.org/licenses/by/4.0/
• Description: This is the standard Creative Commons license that gives others maximum freedom to do what they want with the work as long as they credit the author.

Projects

• Funder: Other - Other funder or multiple funders
• Funding programme: Air Force Office of Scientific Research
• Project number: FA9550-14-1-0096

• Funder: Other - Other funder or multiple funders
• Funding programme: Air Force Office of Scientific Research
• Project number: FA9550-21-1-0024