Fri Jun 15, 2007, 11:00-12:00, 4549 Boelter Hall

An Overview of Dependently Typed Programming

Thorsten Altenkirch
University of Nottingham

Dependent types are types which depend on values, such as the type of
vectors, i.e. lists of a fixed length. Using dependent types we can
statically eliminate run-time errors, like accessing an array out of
range. Exploiting the Curry-Howard equivalence between propositions
and types we can express specifications in types (such as the type of
sorting programs), prove them correct by programming and leave it to
the type checker to certify that we aren't lying.

I will use the Epigram system, a dependently typed programming
language and program development system under development at
Nottingham to illustrate the potential but also the challenges of
dependently typed programming. How practically feasible is dependently
typed programming? What is the role of termination? How to deal with
effects and IO? How to reuse code in a rich type discipline?

About the speaker:
Thorsten Altenkirch is a Reader (Associate Professor) at the School of Computer Science 
and Information Technology of the University of Nottingham.  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-Loef.  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.

Host: Jens Palsberg