Skip to main content


Showing posts from March, 2007


A few months ago I started messing around with The Coq Proof Assistant to figure out what exactly it was, and proceeded to go through the tutorial.

Coq provides a nice interface for doing proofs in an interactive session. It was a lot of fun but didn't seem particularly useful for my research.

As I've been playing with the notion of Total Functional Programming, I ended up reading (and actually doing homework) from a book entitled "Type Theory and Functional Programming". This book is excellent by the way! I highly recommend it to anyone interested in dependent types/proof theory/type theory. It has a very lucid style and makes a lot of complex notions in type theory very easy to understand. I even got to find an error in one of the homework examples (now listed in the errata) which is always fun.

After working through the first 5 chapters I started looking around for a system that would let me apply some of the principles that I had learned.

As it turns ou…