I am Reader (Associate Professor) at the School of Computer Science of the University of Nottingham. Jointly with Graham Hutton I am chairing the Functional Programming Laboratory. We are organizing the weekly FP lunch and the FP seminar.

Here is my entry in the Student guidebook:

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.

*Homotopy Type Theory: Programming and Verification*(joint with Leeds and Strathclyde).

(EPSRC grant EP/M016951/1)

*Reusability and Dependent Types*(joint with Oxford and Strathclyde).

(EPSRC grant EP/G034109/1)*Theory And Applications of Induction Recursion*(joint with Strathclyde and Swansea).

(EPSRC grant EP/G03298X/1)*Modelling Irreversible Quantum Computation*

(EPSRC grant GR/S30818/01)*Midlands Graduate School in the Foundations of Computer Science*

(EPSRC grant GR/T06087/01)*Observational Equality For Dependently Typed Programming*

(EPSRC grant EP/C512022/1)-
*Theory and Applications Of Containers*

(EPSRC Grant: EP/C511964/1)

- Andreas Abel, University of Munich (Germany)
- Jonathan Grattage
- Peter Morris
- James Chapman
- Wouter Swierstra
- Alexander Green
- Rawle Prince
- Iain Lane
- Darin Morrison
- Li Nuo (jointly with Thomas Anberre)
- Nicolai Kraus

I am currently teaching the following modules:

- G52IFR
- Introduction to Formal Reasoning
- G54PRG
- Programming

- G51CSA
- Computer Systems Architecture
- G51MCS
- Mathematics for Computer Scientists
- G51MAL
- Machines and their languages
- G53GEM (with Natasha Alecina)
- Gems of theoretical Computer Science

- October/November 2000
- A Taste of Intuitionistic Type Theory
- February/March 2002
- A Taste of Proof Theory
- March 2003
- Intuitionistic Logic
- March/April 2004
- Lambda calculus and types
- April 2007
- Material for Dependently Typed Programming (DEP)
- April 2008
- Material for the COQ course
- March/April 2009
- Material for the Category Theory course

- Thorsten's quotes, a copy of a web page set up by some of the G51MCS students in 2000.
- Group picture at TLCA 01 in Krakow
- Group picture at APPSEM01 in Darmstadt
- Lambda-Kalkül-und-Typen-Club at the University of Munich (german)
- Conor's course on life under binders
- A poster on our project on Quantum Software, presented at the MathFIT meeting, March 2004.
- Group picture of Dagstuhl seminar 04381 on Dependently Typed Programming. And here Kevin's picture of General Recursion
- Course by Tarmo Uustalu on
*Monads and more*, May 2007 in Nottingham - The page of the workshop Dependently Typed Programming (DTP 2008) which took place in Nottingham in February 2008 with abstracts and slides.
- The page of the workshop Dependently Typed Programming (DTP 2010) which took place in Edinburgh in July 2010.
- Type Theory in Rosario, Course at the University of Rosario, Argentina, July 2011

Last modified: Sat May 23 13:18:53 EEST 2015