All Outputs (10)

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?.

Big Step Normalisation for Type Theory (2020)
Journal Article
Altenkirch, T., & Geniet, C. (2020). Big Step Normalisation for Type Theory. LIPIcs, 2020, Article 4. https://doi.org/10.4230/LIPIcs.TYPES.2019.4

Big step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to... Read More about Big Step Normalisation for Type Theory.

Towards a cubical type theory without an interval (2018)
Journal Article
Altenkirch, T., & Kaposi, A. (2018). Towards a cubical type theory without an interval. LIPIcs, 3:1-3:27. https://doi.org/10.4230/LIPIcs.TYPES.2015.3

Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof... Read More about Towards a cubical type theory without an interval.

Normalisation by evaluation for type theory, in type theory (2017)
Journal Article
Altenkirch, T., & Kaposi, A. (2017). Normalisation by evaluation for type theory, in type theory. Logical Methods in Computer Science, 13(4), https://doi.org/10.23638/LMCS-13%284%3A1%292017

© Altenkirch and Kaposi. We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation henc... Read More about Normalisation by evaluation for type theory, in type theory.

Notions of anonymous existence in Martin-Löf type theory (2017)
Journal Article
Kraus, N., Escardo, M., Coquand, T., & Altenkirch, T. (in press). Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science, 13(1),

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have uniqu... Read More about Notions of anonymous existence in Martin-Löf type theory.

Indexed containers (2015)
Journal Article
Altenkirch, T., Ghani, N., Hancock, P., McBride, C., & Morris, P. (2015). Indexed containers. Journal of Functional Programming, 25, 1-41. https://doi.org/10.1017/s095679681500009x

We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide... Read More about Indexed containers.

Monads need not be endofunctors (2015)
Journal Article
Altenkirch, T., Chapman, J., & Uustalu, T. (2015). Monads need not be endofunctors. Logical Methods in Computer Science, 11(1), 1-40. https://doi.org/10.2168/LMCS-11%281%3A3%292015

We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed ?-calculus syntax and indexed containers. We show tha... Read More about Monads need not be endofunctors.

Relative monads formalised (2014)
Journal Article
Altenkirch, T., Chapman, J., & Uustalu, T. (2014). Relative monads formalised. Journal of Formalized Reasoning, 7(1), https://doi.org/10.6092/issn.1972-5787/4389

Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed... Read More about Relative monads formalised.