Saturday, May 14, 2011

Proving. Things.

I like theorem provers. I also like learning new theorem provers. At this point I'm pretty familiar with Coq and Isabelle, but am still learning Agda.

My first theorem prover was Coq, via Benjamin Pierce's excellent book Software Foundations. Since then, whenever I begin learning a new system I convert proofs and exercises from Pierce's book to the new system I'm learning. I have a decent chunk of the book converted to Isabelle, and the first few chapters in Agda so far.

My advisor has suggested that I attempt to write some kind of internal technical report comparing the advantages and disadvantages of each tool. For example, I might take the simply typed lambda calculus chapters from Software Foundations and write up all the proofs and exercises in each, along with perhaps some of the proofs from Chlipala's book Certified Programming with Dependent types written in Agda. That's right, I want to do some of the proofs he attacks with the crush uber-tactic in Agda. This might be a Poor Life Decision.

I don't expect this to be particularly publishable, but I hope that I can create a bit of a comparative reference of idioms between the three some day that can act as a bit of a mini Rosetta Stone.

Perhaps I can do a bit of the comparisons here on this blog. I haven't entirely decided what I want to use this space for other than to practice writing about technical topics and talking a bit about my PhD work.

No comments:

Post a Comment