Professor THORSTEN ALTENKIRCH's Outputs (27)

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

Constructing a universe for the setoid model (2021)
Presentation / Conference Contribution
Altenkirch, T., Boulier, S., Kaposi, A., Sattler, C., & Sestini, F. (2021, March). Constructing a universe for the setoid model. Presented at 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021), Online

The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent pr... Read More about Constructing a universe for the setoid model.

Big Step Normalisation for Type Theory (2020)
Presentation / Conference Contribution
Altenkirch, T., & Geniet, C. Big Step Normalisation for Type Theory. Presented at 25th International Conference on Types for Proofs and Programs (TYPES 2019), Oslo, Norway

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.

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.

Setoid Type Theory—A Syntactic Translation (2019)
Presentation / Conference Contribution
Altenkirch, T., Boulier, S., Kaposi, A., & Tabereau, N. (2019, October). Setoid Type Theory—A Syntactic Translation. Presented at 13th International Conference on Mathematics of Program Construction (MPC 2019), Porto, Portugal

We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying functional extensionality and propositional extensionality. We justify the rules of setoid type theory by a s... Read More about Setoid Type Theory—A Syntactic Translation.

Constructing quotient inductive-inductive types (2019)
Presentation / Conference Contribution
Kaposi, A., Kovac, A., & Altenkirch, T. (2019, January). Constructing quotient inductive-inductive types. Presented at 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), Cascais/Lisbon, Portugal

Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting... Read More about Constructing quotient inductive-inductive types.

Pure Functional Epidemics: An Agent-Based Approach (2018)
Presentation / Conference Contribution
Thaler, J., Altenkirch, T., & Siebers, P.-O. (2018, September). Pure Functional Epidemics: An Agent-Based Approach. Presented at 30th Symposium on Implementation and Application of Functional Languages, Lowell, Massachusetts, USA

Agent-Based Simulation (ABS) is a methodology in which a system is simulated in a bottom-up approach by modelling the micro interactions of its constituting parts, called agents, out of which the global system behaviour emerges. So far mainly object-... Read More about Pure Functional Epidemics: An Agent-Based Approach.

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)
Book Chapter
Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Forsberg, F. (2018). Quotient inductive-inductive types. In C. Baier, & U. Dal Lago (Eds.), FoSSaCS 2018: Foundations of Software Science and Computation Structures (293-310). Springer Publishing Company. https://doi.org/10.1007/978-3-319-89366-2_16

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.