Research Repository

See what's under the surface


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 2019doi: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

Pure functional epidemics (2018)
Conference Proceeding
Thaler, J., Altenkirch, T., & Siebers, P. (2018). Pure functional epidemics. In IFL'18 Proceedings of 30th Symposium on Implementation and Application of Functional Languages, 5-7 September 2018, Lowell, Mass., 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

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. doi:10.1145/3209108.3209183

Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the higher inductive type F (A)with constructors unit: F(A),cons : A → F(A) → F(A), and conditions saying that every cons(a)is an auto-equivalence on F(A). Equivale... Read More

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:1), doi:10.23638/LMCS-13(4:1)2017. ISSN 1860-5974

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 hence there are no preterms o... Read More

Quotient inductive-inductive types (2017)
Conference Proceeding
Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Forsberg, F. (2017). Quotient inductive-inductive types. In C. Baier, & U. Dal Lago (Eds.), FoSSaCS 2018: Foundations of Software Science and Computation Structures, 293-310. doi: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

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. doi: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

Notions of anonymous existence in Martin-Löf type theory (2016)
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, ISSN 1860-5974

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