My main research interests

Interactive theorem provers based on dependent type theories. Logic and functional programming. Formal program specification.

In short, I work for the brighter future of the brightest programming languages and paradigms. :-)

I am one of those behind the Computational Logic Group.

Current research projects