All Outputs (4)

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.

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). Cham: 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.