logo
School of Computer Science
   
   
  
 

Image of Thorsten Altenkirch

Thorsten Altenkirch

Associate Professor and Reader, Faculty of Science

Contact

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

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

School of Computer Science

University of Nottingham
Jubilee Campus
Wollaton Road
Nottingham, NG8 1BB

telephone: +44 (0) 115 951 4251
fax: +44 (0) 115 951 4254
email: csit-enquiries@cs.nott.ac.uk