All Outputs (3)

The Münchhausen Method in Type Theory (2023)
Journal Article
Altenkirch, T., Kaposi, A., Šinkarovs, A., & Végh, T. (2023). The Münchhausen Method in Type Theory. LIPIcs, 269, https://doi.org/10.4230/LIPIcs.TYPES.2022.10

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 ter... Read More about The Münchhausen Method in Type Theory.

Combinatory logic and lambda calculus are equal, algebraically (2023)
Journal Article
Altenkirch, T., Kaposi, A., Šinkarovs, A., & Végh, T. (2023). Combinatory logic and lambda calculus are equal, algebraically. LIPIcs, Article 24

It is well-known that extensional lambda calculus is equivalent to extensional combinatory logic. In this paper we describe a formalisation of this fact in Cubical Agda. The distinguishing features of our formalisation are the following: (i) Both lan... Read More about Combinatory logic and lambda calculus are equal, algebraically.

Should Type Theory Replace Set Theory as the Foundation of Mathematics? (2023)
Journal Article
Altenkirch, T. (2023). Should Type Theory Replace Set Theory as the Foundation of Mathematics?. Global Philosophy, 33(1), Article 21. https://doi.org/10.1007/s10516-023-09676-0

Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (H... Read More about Should Type Theory Replace Set Theory as the Foundation of Mathematics?.