Finitary type theories with and without contexts

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

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.

• Jezik: Angleški jezik
• Ključne besede: dependent type theory, context-free type theory, formal meta-theory, proof assistants
• Vrsta gradiva: Članek v reviji
• Tipologija: 1.01 - Izvirni znanstveni članek
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Status publikacije: Objavljeno
• Različica publikacije: Objavljena publikacija
• Leto izida: 2023
• Št. strani: 87 str.
• Številčenje: Vol. 67, iss. 4, art. 36
• PID: 20.500.12556/RUL-152580
• UDK: 510.6
• ISSN pri članku: 0168-7433
• DOI: 10.1007/s10817-023-09678-y
• COBISS.SI-ID: 168229379
• Datum objave v RUL: 29.11.2023

Gradivo je del revije

• Naslov: Journal of automated reasoning
• Skrajšan naslov: J. autom. reason.
• Založnik: Springer Nature
• ISSN: 0168-7433
• COBISS.SI-ID: 25709824

Licence

• Licenca: CC BY 4.0, Creative Commons Priznanje avtorstva 4.0 Mednarodna
• Povezava: http://creativecommons.org/licenses/by/4.0/deed.sl
• Opis: To je standardna licenca Creative Commons, ki daje uporabnikom največ možnosti za nadaljnjo uporabo dela, pri čemer morajo navesti avtorja.

Projekti

• Financer: Drugi - Drug financer ali več financerjev
• Program financ.: Air Force Office of Scientific Research
• Številka projekta: FA9550-14-1-0096

• Financer: Drugi - Drug financer ali več financerjev
• Program financ.: Air Force Office of Scientific Research
• Številka projekta: FA9550-21-1-0024