Programming with Dependent Types
Bob Atkey
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.
