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.