coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lambda: The Ultimate TA

From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
To: coq-club AT pauillac.inria.fr
Cc: Study the Masses group on Mechanized Metatheory for <provers AT lists.seas.upenn.edu>
Subject: Re: [Coq-Club] Lambda: The Ultimate TA
Date: Thu, 5 Jun 2008 12:07:10 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

[Reposting with corrected URL -- sorry about that!  -B]

All,

Regular coq-club readers will remember all the questions I was generating in the fall as I grappled with how to best use Coq as the basis for a course on the theory of programming languages. If you are interested in the outcome of all this, you may like to have a look here

  http://www.seas.upenn.edu/~cis500/cis500-f07/schedule.html

at the final version of the course lecture notes (100% Coq!).

I've also written up a short note describing the ups and downs of the experience (there were many of both :-), which can be found here:

  http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf

Best,

    - Benjamin

[Coq-Club] Lambda: The Ultimate TA, Benjamin Pierce
- Re: [Coq-Club] Lambda: The Ultimate TA, Benjamin Pierce