I am Reader (Associate Professor) at the School of Computer Science of the University of Nottingham. Graham Hutton and myself have recently started our own group: the Functional Programming Laboratory.
The 3rd workshop in the PLPV series aimed at providing a forum for researchers from different research communities (language based / logic based, US / EU, ...). The meeting will be affiliated with POPL in January 2009, please submit your papers before 8 October.
Tarmo Uustalu and I are editing a special issue of Fundamenta Informaticae on DTP. The deadline is 1 October 2008. Please submit - here is the CFP
On an international level I am active in the ESPRIT working groups Computer-Assisted Reasoning based on Type Theory and Applied Semantics.
Here is my entry in the Student guidebook:
Keywords: Constructive Logic, Type Theory, Category Theory, Lambda calculus, Quantum Computing, Certified Correct ProgramsThorsten 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.
I am currently teaching the following modules: