TY - GEN
T1 - The Münchhausen Method in Type Theory
AU - Altenkirch, Thorsten
AU - Kaposi, Ambrus
AU - Šinkarovs, Artjoms
AU - Végh, Tamás
N1 - Funding Information:
Funding Ambrus Kaposi: Supported by the “Application Domain Specific Highly Reliable IT Solutions” project which has been implemented with support from the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme TKP2020-NKA-06 (National Challenges Subprogramme) funding scheme, and by Bolyai Scholarship BO/00659/19/3. Artjoms Šinkarovs: Supported by the Engineering and Physical Sciences Research Council through the grant EP/N028201/1.
Publisher Copyright:
© Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh.
PY - 2023/7/28
Y1 - 2023/7/28
N2 - In one of his long tales, after falling into a swamp, Baron Münchhausen salvaged himself and the horse by lifting them both up by his hair. Inspired by this, the paper presents a technique to justify very dependent types. Such types reference the term that they classify, e.g.x : F x. While in most type theories this is not allowed, we propose a technique on salvaging the meaning of both the term and the type. The proposed technique does not refer to preterms or typing relations and works in a completely algebraic setting, e.g categories with families. With a series of examples we demonstrate our technique. We use Agda to demonstrate that our examples are implementable within a proof assistant.
AB - In one of his long tales, after falling into a swamp, Baron Münchhausen salvaged himself and the horse by lifting them both up by his hair. Inspired by this, the paper presents a technique to justify very dependent types. Such types reference the term that they classify, e.g.x : F x. While in most type theories this is not allowed, we propose a technique on salvaging the meaning of both the term and the type. The proposed technique does not refer to preterms or typing relations and works in a completely algebraic setting, e.g categories with families. With a series of examples we demonstrate our technique. We use Agda to demonstrate that our examples are implementable within a proof assistant.
KW - proof assistants
KW - type theory
KW - very dependent types
UR - http://www.scopus.com/inward/record.url?scp=85169293667&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.TYPES.2022.10
DO - 10.4230/LIPIcs.TYPES.2022.10
M3 - Conference contribution
AN - SCOPUS:85169293667
T3 - Leibniz International Proceedings in Informatics
BT - 28th International Conference on Types for Proofs and Programs (TYPES 2022)
A2 - Kesner, Delia
A2 - Pedrot, Pierre-Marie
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
T2 - 28th International Conference on Types for Proofs and Programs 2022
Y2 - 20 June 2022 through 25 June 2022
ER -