Thorsten Altenkirch

I am 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.

How to contact me ?

Recent talks

Drafts and Publications (my page), google scholar page

Current Research grants

• 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)

Previous Research grants

• 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)

PhD students

Former Students

• 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

Current Students

• Gabe Dijkstra
• Jakob von Raumer

Current Teaching

I am currently teaching the following modules:

G52IFR

Introduction to Formal Reasoning

G54PRG

Programming

Previous Teaching

G51CSA

Computer Systems Architecture

• description
• course page

G51MCS

Mathematics for Computer Scientists

• description
• course page

G51MAL

Machines and their languages

• description
• course page

G53GEM (with Natasha Alecina)

Gems of theoretical Computer Science

• description
• course page

Midlands Graduate School

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

Misc

• 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.