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.

*Certified Programming with Dependent Types*USAF, Airforce office for scientific research, award FA9550-16-1-0029*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
- Lecture notes for the course Introduction to Homotopy Type Theory at the Estonian Winter School in Computer Science 2017.

Last modified: Fri Mar 24 13:33:51 GMT 2017