Hello,

I’d like to invite you all to join a summer reading and research group with Dan Friedman. The group will meet multiple days each week; we will try to arrange times and location so that everyone interested can attend.

Dan’s current PL-related research is about theorem proving and theorem generation. We invite those who wish to join us in a group whose purpose will be to work with Coq (http://coq.inria.fr/) and possibly Agda (http://wiki.portal.chalmers.se/agda/). We will begin with the introductory tutorial Coq in a Hurry by Yves Bertot (http://cel.archives-ouvertes.fr/inria-00001173/).

Our group will also read Interactive Theorem Proving and Program Development by Yves Bertot and Pierre Casteran (http://www.labri.fr/perso/casteran/CoqArt/) and Software Foundations by Benjamin Pierce, et al (http://www.seas.upenn.edu/~cis500/current/sf/html/). We may read certain passages aloud, and will ask and (attempt to) answer any questions as we go, so that everyone understands the reading fully.

Our aim is to implement a subset of some Proof Assistant, be it a Coquette or miniAgda, so we will really have to understand the material completely. Once we understand Coq and/or Agda at a deep enough level, we hope to either add to mini/αKanren some of the ideas we have learned, or build a Coquette or miniAgda that allows us to explain in simpler terms what is involved in its understanding.


Thank you,
Adam Foltzer