All Outputs (26)

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), 1-40. https://doi.org/10.2168/LMCS-11%281%3A3%292015

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

Relative monads formalised (2014)
Journal Article
Altenkirch, T., Chapman, J., & Uustalu, T. (2014). Relative monads formalised. Journal of Formalized Reasoning, 7(1), https://doi.org/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.

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.

When is a function a fold or an unfold? (2001)
Conference Proceeding
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?.

Representations of first order function types as terminal coalgebras (2001)
Conference Proceeding
Altenkirch, T. (2001). Representations of first order function types as terminal coalgebras.