APL18: Guest Lecture

Programming with Dependent Types

Bob Atkey

University of Edinburgh

9am Thursday March 12th 2009

Dependent types extend normal type systems by allowing values to appear in types. This facility is extremely powerful and allows the definition of refined types that capture properties of data that are not expressible in normal type systems. A simple example is the type of lists of a length n, with an append function of type:

forall m n, list m -> list n -> list (m + n)

In this talk I will show how to use the Coq system to write programs with dependent types, and how they can be extracted to normal OCaml code, compiled, and run.

Comments are closed.