Skip to main content

Research Repository

Advanced Search

All Outputs (15)

Combinatory logic and lambda calculus are equal, algebraically (2023)
Presentation / Conference Contribution
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.

Constructing a universe for the setoid model (2021)
Presentation / Conference Contribution
Altenkirch, T., Boulier, S., Kaposi, A., Sattler, C., & Sestini, F. (2021). Constructing a universe for the setoid model. In S. Kiefer, & C. Tasson (Eds.), Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings (1-21). https://doi.org/10.1007/978-3-030-71995-1_1

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

The Integers as a Higher Inductive Type (2020)
Presentation / Conference Contribution
Altenkirch, T., & Scoccola, L. (2020). The Integers as a Higher Inductive Type. In LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (67-73). https://doi.org/10.1145/3373718.3394760

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.

Setoid Type Theory—A Syntactic Translation (2019)
Presentation / Conference Contribution
Altenkirch, T., Boulier, S., Kaposi, A., & Tabereau, N. (2019). Setoid Type Theory—A Syntactic Translation. In Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings (155-196). https://doi.org/10.1007/978-3-030-33636-3_7

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). Constructing quotient inductive-inductive types. In Proceedings of the ACM on Programming Languages archive Volume 3 Issue POPL, January 2019 (1-24). https://doi.org/10.1145/3290315

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). Pure Functional Epidemics: An Agent-Based Approach. In IFL'18 Proceedings of 30th Symposium on Implementation and Application of Functional Languages, 5-7 September 2018, Lowell, Mass., USA (1-12). https://doi.org/10.1145/3310232.3310372

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). Free Higher Groups in Homotopy Type Theory. In LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (599-608). https://doi.org/10.1145/3209108.3209183

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

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.

Type theory in type theory using quotient inductive types (2016)
Presentation / Conference Contribution
Altenkirch, T., & Kaposi, A. (2016). Type theory in type theory using quotient inductive types. In POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (18-29). https://doi.org/10.1145/2837614.2837638

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.

Some constructions on ω-groupoids (2014)
Presentation / Conference Contribution
Altenkirch, T., Li, N., & Ondřej, R. (2014). Some constructions on ω-groupoids. . https://doi.org/10.1145/2631172.2631176

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

Generalizations of Hedberg’s Theorem (2013)
Presentation / Conference Contribution
Kraus, N., Escardó, M., Coquand, T., & Altenkirch, T. (2013). Generalizations of Hedberg’s Theorem. In Typed Lambda Calculi and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June (173-188). https://doi.org/10.1007/978-3-642-38946-7_14

As the groupoid interpretation by Hofmann and Streicher shows, uniqueness of identity proofs (UIP) is not provable. Generalizing a theorem by Hedberg, we give new characterizations of types that satisfy UIP. It turns out to be natural in this context... Read More about Generalizations of Hedberg’s Theorem.

When is a function a fold or an unfold? (2001)
Presentation / Conference Contribution
Gibbons, J., Hutton, G., & Altenkirch, T. (2001). When is a function a fold or an unfold?.

We give a necessary and sufficient condition for when a set-theoretic function can be written using the recursion operator fold, and a dual condition for the recursion operator unfold. The conditions are simple, practically useful, and generic in the... Read More about When is a function a fold or an unfold?.