Programming with Proofs

Recent developments in the area of expressive types, e.g. generalized algebraic data types (GADTs) and type classes with extensions, have the prospect to supply the ordinary programmer with a programming language rich enough to verify complex program properties. Program verification is made possible via type checking. In [4], I explored this possibility and critically assess the current state of the art.

The work here builds largely upon previous work where I introduced expressive types as data types with extensions. The Chameleon language implements the idea of expressive types. Similar languages/systems are Hongwei Xi's ATS and Tim Sheard's Omega.

In another direction, I explored the impact expressive type information has on a type-preserving compiler. In [2], I co-designed an extension of System F rich enough to host the typed-intermediate language of the Glasgow Haskell Compiler (GHC) with extensions.

Martin Sulzmann 2006-07-19