Skip to main content

Research Repository

See what's under the surface


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, Proceedingshttps://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.

Naive Type Theory (2019)
Book Chapter
Altenkirch, T. (in press). Naive Type Theory. In S. Centrone, D. Kant, & D. Sarikaya (Eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General ThoughtsSpringer

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.

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 about Constructing quotient inductive-inductive types.

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, 1-12. doi: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.

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

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

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 about Normalisation by evaluation for type theory, in 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. 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 about Partiality, revisited: the partiality monad as a quotient inductive-inductive type.

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 about Notions of anonymous existence in Martin-Löf type theory.

Extending homotopy type theory with strict equality (2016)
Conference Proceeding
Altenkirch, T., Capriotti, P., & Nicolai, K. (in press). Extending homotopy type theory with strict equality

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

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.

Monads need not be endofunctors (2015)
Journal Article
Altenkirch, T., Chapman, J., & Uustalu, T. (2015). Monads need not be endofunctors. Logical Methods in Computer Science, 11(1:3), doi:10.2168/LMCS-11(1:3)2015

We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed λ-calculus syntax and indexed containers. We show tha... Read More about Monads need not be endofunctors.

Some constructions on ω-groupoids (2014)
Conference Proceeding
Altenkirch, T., Li, N., & Ondřej, R. (2014). Some constructions on ω-groupoids. doi: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.

Relative monads formalised (2014)
Journal Article
Altenkirch, T., Chapman, J., & Uustalu, T. (2014). Relative monads formalised. Journal of Formalized Reasoning, 7(1), doi:10.6092/issn.1972-5787/4389

Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed... Read More about Relative monads formalised.