Thorsten Altenkirch

Contact

• workRoom C35 Computer Science
  Jubilee Campus
  Wollaton Road
  Nottingham
  NG8 1BB
  UK
• workn/a
• Thorsten.Altenkirch@nottingham.ac.uk
• http://www.cs.nott.ac.uk/~txa/

Research Summary

Thorsten Altenkirch's main research interest is the application of constructive logic in Computer Science. Constructive logic diverges from classical logic in the rejection of the principle of the… read more

Selected Publications

• ABBOTT, M., ALTENKIRCH, T. and GHANI, N., 2005. Containers: constructing strictly positive types Theoretical Computer Science. 342(1), 3-27
• ABBOTT, M., ALTENKIRCH, T., MCBRIDE, C. and GHANI, N., 2005. ∂ for Data: differentiating data structures Fundamentae Informatica. 65(1/2), 1-28
• ALTENKIRCH, T. and GRATTAGE, J., 2005. A functional quantum programming language In: 20th Annual IEEE Symposium on Logic in Computer Science, Chicago, USA, 26-29 June 2005. 249-259
• ALTENKIRCH, T., DYBJER, P., HOFMANN, M. and SCOTT, P., 2001. Normalization by Evaluation for Typed Lambda Calculus with Coproducts In: 16th Annual IEEE Symposium on Logic in Computer Science.

• View all publications

Current Research

Thorsten Altenkirch's main research interest is the application of constructive logic in Computer Science. Constructive logic diverges from classical logic in the rejection of the principle of the excluded middle. As a consequence of this, a constructive proof of the existence of a certain object (e.g. a number) can be turned into a computer program to calculate this object.An example of a constructive logic is Type Theory, introduced by the Swedish philosopher Per Martin-Löf. Type Theory is at the same time a programming language and a logic: propositions correspond to types and proofs to programs. Current research centers on theoretical aspects of Type Theory but also on the construction of elegant and efficient implementations of type theoretic languages. An example of this is the Epigram system, currently under development in Nottingham, which we use to develop programs which are correct by construction.Dr. Altenkirch's research covers applications of Category Theory as a formalism to concisely express abstract properties of mathematical constructions in Computer Science and the investigation of typed lambda calculi as a foundation of (functional) programming languages and Type Theory. He is interested in the computational nature of the physical universe and the practical exploitation of this nature, which is reflected in a research project on Quantum Computation. He is also fascinated by the development of the philosophical foundations of logic in a time when computing science replaces natural science as the prime application of abstract reasoning.For further information about his research, please consult his homepage.

• THORSTEN ALTENKIRCH, NILS ANDERS DANIELSSON and NICOLAI KRAUS, 2017. Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type In: Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. 534-549
• THORSTEN ALTENKIRCH and AMBRUS KAPOSI, 2017. Normalisation by Evaluation for Type Theory, in Type Theory Logical Methods in Computer Science. 13(4),
• THORSTEN ALTENKIRCH, PAOLO CAPRIOTTI, GABE DIJKSTRA, NICOLAI KRAUS and FREDRIK NORDVALL FORSBERG, 2017. Quotient inductive-inductive types
• ALTENKIRCH, THORSTEN and KAPOSI, AMBRUS, 2016. Type theory in type theory using quotient inductive types ACM SIGPLAN Notices. 51(1), 18-29
• THORSTEN ALTENKIRCH and AMBRUS KAPOSI, 2016. Normalisation by Evaluation for Dependent Types In: 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. 6:1-6:16
• THORSTEN ALTENKIRCH, PAOLO CAPRIOTTI and NICOLAI KRAUS, 2016. Extending Homotopy Type Theory with Strict Equality In: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France. 21:1-21:17
• THORSTEN ALTENKIRCH, JAMES CHAPMAN and TARMO UUSTALU, 2015. Monads Need Not Be Endofunctors Logical Methods in Computer Science. 11(1:3), 1-40
• ALTENKIRCH, THORSTEN, LI, NUO and RYP'AVCEK, ONDVREJ, 2014. Some Constructions on omega-groupoids In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. 4:1-4:8
• THORSTEN ALTENKIRCH, JAMES CHAPMAN and TARMO UUSTALU, 2014. Relative Monads Formalised J. Formalized Reasoning. 7(1), 1-43
• NICOLAI KRAUS, MART'IN HÖTZEL ESCARDÓ, THIERRY COQUAND and THORSTEN ALTENKIRCH, 2013. Generalizations of Hedberg's Theorem In: Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013. 173-188
• PETER HANCOCK, CONOR MCBRIDE, NEIL GHANI, LORENZO MALATESTA and THORSTEN ALTENKIRCH, 2013. Small Induction Recursion In: Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013. 156-172
• THORSTEN ALTENKIRCH and ONDREJ RYPACEK, 2012. A Syntactical Approach to Weak omega-Groupoids In: Computer Science Logic (CSL'12). 16-30
• THORSTEN ALTENKIRCH, FREDRIK NORDVALL FORSBERG, PETER MORRIS and ANTON SETZER, 2011. A categorical semantics for inductive-inductive definitions. In: Fourth International Conference on Algebra and Coalgebra in Computer Science: CALCO 2011
• ALTENKIRCH, T. and GREEN, A., 2010. The Quantum IO monad. In: GAY, S. and MACKIE, I., eds., Semantic techniques in quantum computation Cambridge University Press. 173-205
• ALTENKIRCH, T., CHAPMAN, J. and UUSTALU, T., 2010. Monads need not be endofunctors. In: ONG, L., ed., Foundations of software science and computational structures: 13th international conference, FOSSACS 2010, held as part of the joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010 : proceedings Springer. 297-311
• THORSTEN ALTENKIRCH, NILS ANDERS DANIELSSON, ANDRES LÖH and NICOLAS OURY, 2010. PiSigma: Dependent Types without the Sugar. In: Functional and Logic Programming Springer. 40-55
• THORSTEN ALTENKIRCH, PAUL LEVY and SAM STATON, 2010. Higher Order Containers. In: Computability in Europe: CiE 2010
• ALTENKIRCH, T. and CHAPMAN, J., 2009. Big-step normalisation Journal of Functional Programming. 19(3-4), 311-333
• ALTENKIRCH, T. and MORRIS, P., 2009. Indexed containers In: 24th Annual IEEE Symposium on Logic in Computer Science. 277-285
• MORRIS, P., ALTENKIRCH, T. and GHANI, N., 2007. Constructing Strictly Positive Families In: The Australasian Theory Symposium. 111-122
• ALTENKIRCH, T., GRATTAGE, J., VIZZOTTO, J.K. and SABRY A., 2007. An Algebra of Pure Quantum Programming Electronic Notes in Theoretical Compter Science: 3rd International Workshop on Quantum Programming Languages. 170C, 23-47 (In Press.)
• VIZZOTTO, J., ALTENKIRCH, T. and SABRY, A., 2006. Structuring quantum effects: superoperators as arrows Mathematical Structures in Computer Science. 16(3), 453-468
• MORRIS, P., ALTENKIRCH, T. and MCBRIDE, C., 2006. Exploring the Regular Tree Types In: Types for Proofs and Programs.
• ABBOTT, M., ALTENKIRCH, T. and GHANI, N., 2005. Containers: constructing strictly positive types Theoretical Computer Science. 342(1), 3-27
• ABBOTT, M., ALTENKIRCH, T., MCBRIDE, C. and GHANI, N., 2005. ∂ for Data: differentiating data structures Fundamentae Informatica. 65(1/2), 1-28
• ALTENKIRCH, T. and GRATTAGE, J., 2005. A functional quantum programming language In: 20th Annual IEEE Symposium on Logic in Computer Science, Chicago, USA, 26-29 June 2005. 249-259
• ABBOTT, M., ALTENKIRCH, T. and GHANI, N., 2004. Representing Nested Inductive Types using W-types In: Automata, Languages and Programming. 59 - 71
• ALTENKIRCH, T. and UUSTALU, T., 2004. Normalization by evaluation for λ→2 In: Functional and Logic Programming. 260 - 275
• ABBOTT, M., ALTENKIRCH, T., GHANI, N. and MCBRIDE, C., 2004. Constructing Polymorphic Programs with Quotient Types In: 7th International Conference on Mathematics of Program Construction.
• ABOTT, M., ALTENKIRCH, T. and GHANI, N., 2003. Categories of containers. In: GORDON, A.D., ed., Foundations of software science and computational structures: 6th International Conference, FOSSACS 2003, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003: proceedings Berlin: Springer. 23-38
• ABOTT, M., ALTENKIRCH, T., GHANI, N. and MCBRIDE, C., 2003. Derivatives of Containers In: Typed Lambda Calculi and Applications, TLCA 2003.
• ABEL, A. and ALTENKIRCH, T., 2002. A predicative analysis of structural recursion Journal of Functional Programming. 12(1), 1-41
• ALTENKIRCH, T. and MCBRIDE, C., 2002. Generic Programming within Dependently Typed Programming In: Proceedings IFIP Working Conference on Generic Programming.
• GIBBONS, J., HUTTON, G.M. and ALTENKIRCH, T., 2001. When is a Function a Fold or an Unfold? In: Proceedings of the 4th International Workshop on Coalgebraic Methods in Computer Science.
• ALTENKIRCH, T., DYBJER, P., HOFMANN, M. and SCOTT, P., 2001. Normalization by Evaluation for Typed Lambda Calculus with Coproducts In: 16th Annual IEEE Symposium on Logic in Computer Science.
• ALTENKIRCH, T. and COQUAND, T., 2001. A Finitary Subsystem of the Polymorphic Lambda-Calculus In: Typed Lambda Calculi and Applications. 22-28
• THORSTEN ALTENKIRCH and AMBRUS KAPOSI, Towards a cubical type theory without an interval Leibniz International Proceedings in Informatics.