nLab Thorsten Altenkirch

Thorsten Altenkirch is an associate professor for computer science at University of Nottingham.

• webpage

Talks

• Towards higher dimensional type theory, Nottingham (2011) (pdf)

Selected writings

On inductive types and W-types:

• Michael Abbott, Thorsten Altenkirch, Neil Ghani: Representing Nested Inductive Types using W-types, in: Automata, Languages and Programming, ICALP 2004, Lecture Notes in Computer Science, 3142, Springer (2004) [doi:10.1007/978-3-540-27836-8_8, pdf]

  exposition: Inductive Types for Free – Representing nested inductive types using W-types, talk at ICALP (2004) [pdf]

Introducing the quantum programming language QML:

• Thorsten Altenkirch, Jonathan Grattage, A functional quantum programming language, Logic in Computer Science, 2005. Proceedings. 20th Annual IEEE Symposium on, 26-29 June 2005 249 - 258 (arXiv:quant-ph/0409065, doi:10.1109/LICS.2005.1, pdf)

Introducing the quantum IO monad:

• Thorsten Altenkirch, The Quantum IO Monad, Nottingham (2006) [pdf, pdf]

• Thorsten Altenkirch, Alexander Green, The quantum IO monad, Ch. 5 of: Simon Gay, Ian Mackie (eds.): Semantic Techniques in Quantum Computation (2010) 173-205 [pdf, doi:10.1017/CBO9781139193313.006]

Introducing relative monads in computer science:

• Thorsten Altenkirch, James Chapman, Tarmo Uustalu, Monads need not be endofunctors, Logical Methods in Computer Science 11 1:3 (2015) 1–40 [arXiv:1412.7148, pdf, doi:10.2168/LMCS-11(1:3)2015]

On weakly constant functions and propositional truncation in homotopy type theory:

• Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch, Notions of Anonymous Existence in Martin-Löf Type Theory, Logical Methods in Computer Science 13 1 [doi:10.23638/LMCS-13(1:15)2017, arXiv:1610.03346]

On quotient inductive types:

• Thorsten Altenkirch, Nils A. Danielsson, Nicolai Kraus, Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type, FoSSaCS 2017, Lecture Notes in Computer Science 10203 Springer (2017) [arXiv:1610.09254]

On free groups and $\infty$-groups in homotopy type theory:

• Nicolai Kraus, Thorsten Altenkirch, Free Higher Groups in Homotopy Type Theory, LICS ‘18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, (2018) [arXiv;1805.02069, doi:10.1145/3209108.3209183]

On quotient types and higher inductive types:

• Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Forsberg, Quotient inductive-inductive types, Foundations of Software Science and Computation Structures (FoSSaCS 2018), Lecture Notes in Computer Science 10803 (2018) [doi:10.1007/978-3-319-89366-2_16, arXiv:1612.02346]

On the prehistory of homotopy type theory and the univalence axiom in the hands of Martin Hofmann:

• Thorsten Altenkirch, Martin Hofmann’s contributions to type theory: Groupoids and univalence, Mathematical Structures in Computer Science 31 9 (2021) 953-957 [doi:10.1017/S0960129520000316]

Related entries

• type theory, homotopy type theory

• verified software

• categorical model of dependent types

category: people