Skip to main content

Research Repository

Advanced Search

All Outputs (14)

Constructing a universe for the setoid model (2021)
Conference Proceeding
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.

The Integers as a Higher Inductive Type (2020)
Conference Proceeding
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)
Conference Proceeding
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)
Conference Proceeding
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)
Conference Proceeding
Thaler, J., Altenkirch, T., & Siebers, P. (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)
Conference Proceeding
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)
Conference Proceeding
Altenkirch, T., Danielson, N. A., & Kraus, N. (2017). Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. In Foundations of Software Science and Computation Structures: FoSSaCS 2017 (534-549). https://doi.org/10.1007/978-3-662-54458-7_31

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,... Read More about Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.

Extending Homotopy Type Theory with Strict Equality (2016)
Conference Proceeding
Altenkirch, T., Capriotti, P., & Kraus, N. (2016). Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (21:1-21:17). https://doi.org/10.4230/LIPIcs.CSL.2016.21

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.

Type theory in type theory using quotient inductive types (2016)
Conference Proceeding
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.

Generalizations of Hedberg’s Theorem (2013)
Conference Proceeding
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.