Types
Saturday, August 16th, 2008Since learning about the Curry-Howard isomorphism, I’ve been looking more closely at type theory, starting with the freely available and well-written book, Type Theory and Functional Programming. But now, I’ve been wanting to play with some type systems more. I looked at LambdaPi, which prompted me to review my basics. So I jumped to Pierce’s class, Software Foundations, which he discusses in Lambda The Ultimate TA. The lectures/scripts are a great and simple way to learn Coq. I’ve only just finished lecture 3, and I finally understand Coq’s role as a proof assistant. I am planning to work through the entire set of lectures.