How to write your next POPL paper in Coq

If this sounds like a worthy goal, or if you are simply interested in the use of proof assistants for rogramming language research, you don't want to miss upcoming tutorial.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Publishing the tutorial?

You're right, I don't want to miss the tutorial! Unfortunately I live on the East Coast and won't be able to make the conference. Is there any chance you'll be publishing the slides after the presentation? I've been interested in Coq and other theorem provers for a few months now but have found them difficult to approach. Can anyone recommend any other tutorials for using proof assistants with respect to programming language research?


We will be publishing online the materials (slides, exercises, etc.) for the tutorial afterwards. We're aiming to make the materials useful both for those who do attend the tutorial (e.g., additional exercises we won't have time to get to) and for those who are looking at them "off-line" (e.g., plenty of written comments and explanations).

(Just to be clear, I am one of the many people helping organize this tutorial.)

Course on Coq

Take a look at this post, including comments. You should find a few more pointers to tutorials and ideas about how to begin studying.

You Had Better Believe...

...I'm going. With bells on.

Can someone say something about the prerequisites?

I guess the easiest way to answer this would be to point me at some papers that I'd have to understand to be able to make sense of this course.

A Syntactic Approach to Type

See also here (and revive

See also here (and revive the old thread if you want).

My Opinion...

...about a useful introductory path can be found here.

In particular...

...get the Coq'Art book. Do spend the money, if you will spend the time.

Tutorial materials

Are here.

U Penn CIS 500 Materials

According to Michael Greenberg (hi, Michael! It was nice to meet you at the tutorial), U Penn's CIS 500 course covers essentially the same material as the tutorial did—it just does so in a semester rather than one day. :-) The CIS 500 course materials can be found here. What's perhaps a bit confusing at first is that the "lectures" linked to are, in fact, Coq .v files.

I should point out that all of these Coq developments are extremely heavily commented and the introductory materials (CoqIntro.v, STLCTutorial.v) are self-contained: it's possible to work through them without reference to anything else and they assume no prior experience. They also reflect the high writing standards that we've come to expect from the Computer Science department at U Penn.

In summary, the in-person tutorial at POPL '08 was exactly the breakneck-paced, whirlwind slide down the rabbit hole that I had hoped it would be—honestly, I can't recall the last time I had that panicky I'm-falling-behind-and-I'll-never-catch-up feeling and paid good money for it. The last time I was in school, I suppose. :-) The U Penn team were well-prepared, with printouts; CDs containing all of the software, documentation, IDEs, and tutorial files; and tremendous patience with us newcomers. The pace really was breakneck, but it had to be given the scope: zero to progress and preservation for the simply-typed lambda calculus in one day. Somehow, though, they seemed to keep their fingers on the pulse of the group, dropping exercises, giving a few more minutes for people to complete their work, helping out both during the exercise time and during breaks, etc.

For those who are interested but couldn't attend, I can't recommend the tutorial materials proper and U Penn's CIS 500 materials strongly enough. It's also worth keeping in mind that in some ways, this really was the coming-out party for U Penn's metatheory library for Coq, which has already seen third-party use and gotten positive feedback, as I commented on here.