Thorsten Altenkirch is a professor of computer science at the University of Nottingham.
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 observational type theory:
Thorsten Altenkirch, Conor McBride, Towards observational type theory, draft (2006) [pdf, pdf, pdf]
Thorsten Altenkirch, Conor McBride, Wouter Swierstra, Observational Equality, Now!, PLPV ‘07: Proceedings of the 2007 workshop on Programming languages meets program verification (2007) 57-68 [ISBN:978-1-59593-677-6, doi:10.1145/1292597.1292608, pdf]
Introducing the quantum programming language QML:
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:
On weakly constant functions and propositional truncation in homotopy type theory:
On free groups and -groups in homotopy type theory:
On quotient types and higher inductive types:
On the prehistory of homotopy type theory and the univalence axiom in the hands of Martin Hofmann:
A fragment of higher observational type theory
On naive/informal dependent type theory:
Last revised on January 15, 2025 at 17:53:25. See the history of this page for a list of all contributions to it.