Lambda the Ultimate

Postdoc at Harvard.
Former PhD student in Computer Science at LRI (http://www.lri.fr).
I work on programming and proving with dependent types in the Coq proof assistant.

Functional programming, type theory and type systems.