Coq

About 7 months ago I started exploring new theorem provers for use in my lab and teaching. I am a diehard PVS fan and that really hasn’t changed. The folks at SRI produced a tool that shaped my teaching and research for years. I just got a bit stir crazy and wanted to check out something completely different.

Enter Coq. I’ve been fascinated by my PL friends obsession with the tool generally and the application or Curry-Howard specifically, so I started through Pierce’s Software Foundations and later Chlipala’s Certified Programming with Dependent Types to learn more. In a word, I’m hooked. I’ve moved my formal methods class to Coq as well as my current research projects. I’m not yet as productive in Coq as I am in PVS, but I’m getting there.

I don’t yet have anything significant to offer the Coq community in thanks. I hope to develop an undergraduate online text, but that’s a ways off. For now, I will do several blog entries that capture my learning process, things I’ve found interesting, and some teaching experiences with the tool. If you find any of this useful, give me a shout. More importantly, if anything is wrong, give me a shout.