Professor THORSTEN ALTENKIRCH's Outputs (23)

Internal Parametricity, without an Interval (2024)
Journal Article
Altenkirch, T., Chamoun, Y., Kaposi, A., & Shulman, M. (2024). Internal Parametricity, without an Interval. Proceedings of the ACM on Programming Languages, 8(POPL), 2340-2369. https://doi.org/10.1145/3632920

Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it... Read More about Internal Parametricity, without an Interval.

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)
Presentation / Conference Contribution
Altenkirch, T., Kaposi, A., Šinkarovs, A., & Végh, T. Combinatory logic and lambda calculus are equal, algebraically. Presented at FSCD, Rome, Italy

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

Martin Hofmann’s Contributions to Type Theory: Groupoids and Univalence (2021)
Journal Article
Altenkirch, T. (2021). Martin Hofmann’s Contributions to Type Theory: Groupoids and Univalence. Mathematical Structures in Computer Science, 31(9), 953-957. https://doi.org/10.1017/S0960129520000316

My goal is to give an accessible introduction to Martin’s work on the groupoid model and how it is related to the recent notion of univalence in Homotopy Type Theory while sharing some memories of Martin.

The Integers as a Higher Inductive Type (2020)
Presentation / Conference Contribution
Altenkirch, T., & Scoccola, L. (2020, July). The Integers as a Higher Inductive Type. Presented at LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken Germany

We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to... Read More about The Integers as a Higher Inductive Type.

Naive Type Theory (2019)
Book Chapter
Altenkirch, T. (2019). Naive Type Theory. In S. Centrone, D. Kant, & D. Sarikaya (Eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts (101-136). Springer

We introduce Type Theory, including Homotopy Type Theory, as an alternative to set theory as a foundation of Mathematics emphasising the intuitive and naive understanding of its concepts.

Free Higher Groups in Homotopy Type Theory (2018)
Presentation / Conference Contribution
Kraus, N., & Altenkirch, T. (2018, July). Free Higher Groups in Homotopy Type Theory. Presented at LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford United Kingdom

© 2018 ACM. Given a type A in homotopy type theory (HoTT), we can define the free∞-group onA as the loop space of the suspension ofA+1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit : F(A),... Read More about Free Higher Groups in Homotopy Type Theory.

Quotient inductive-inductive types (2018)
Presentation / Conference Contribution
Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Forsberg, F. (2018, April). Quotient inductive-inductive types. Presented at 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece

Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the sense of H... Read More about Quotient inductive-inductive types.

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.

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (2017)
Presentation / Conference Contribution
Altenkirch, T., Danielson, N. A., & Kraus, N. (2017, April). Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. Presented at 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, Uppsala, Sweden

Capretta’s delay monad can be used to model partial computations, but it has the “wrong” notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the “right” notion of equality, weak bisimilarity. However, re... Read More about Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.

Extending Homotopy Type Theory with Strict Equality (2016)
Presentation / Conference Contribution
Altenkirch, T., Capriotti, P., & Kraus, N. (2016, August). Extending Homotopy Type Theory with Strict Equality. Presented at 25th EACSL Annual Conference on Computer Science Logic, CSL 2016., Marseille, France

In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult a... Read More about Extending Homotopy Type Theory with Strict Equality.

Normalisation by evaluation for dependent types (2016)
Presentation / Conference Contribution
Altenkirch, T., & Kaposi, A. Normalisation by evaluation for dependent types. Presented at FSCD 2016: 1st International Conference on Formal Structures for Computation and Deduction

We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realiz... Read More about Normalisation by evaluation for dependent types.

Type theory in type theory using quotient inductive types (2016)
Presentation / Conference Contribution
Altenkirch, T., & Kaposi, A. (2016, January). Type theory in type theory using quotient inductive types. Presented at POPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St Petersburg, Florida, USA

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids r... Read More about Type theory in type theory using quotient inductive types.

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.

Some constructions on ω-groupoids (2014)
Presentation / Conference Contribution
Altenkirch, T., Li, N., & Ondřej, R. (2014, July). Some constructions on ω-groupoids. Presented at LFMTP '14: Theory and Practice, Vienna, Austria

Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the constructive semantics of Homotopy Type Theory [13]. Following up on our previous formalisation [3] and Brunerie's notes [6], we present a ne... Read More about Some constructions on ω-groupoids.

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.