[TYPES/announce] Coq tutorial materials available

[Stephanie Weirich]

Reminder: the Coq Tutorial is next Tuesday in San Francisco, and the
schedule is now on the webpage.

If you will be attending the tutorial, please download the tutorial
materials and try to compile them before coming to the tutorial.

If you cannot attend, all of the materials for the tutorial are
now available on the webpage and are self contained. You are welcome
and encouraged to step through them on your own.

Thanks and see you in San Francisco,

  Stephanie

=====================================================================

               Tutorial Announcement and Call for Participation


           Using Proof Assistants for Programming Language Research
                                     Or:
                   How to Write Your Next POPL Paper in Coq

                        San Francisco, CA, 8 Jan 2008
                          Co-located with POPL 2008
                           Sponsored by ACM SIGPLAN

                     http://plclub.org/popl08-tutorial/

=======================================================================

The University of Pennsylvania PLClub invites you to participate in a
tutorial on using the Coq proof assistant to formalize programming
language metatheory.

This tutorial will be tailored to people who are familiar with syntactic
proofs of programming language metatheory (type soundness, etc.), but
have never used a proof assistant. At the end of the day, participants
will have a reading knowledge of Coq and a running start on using Coq
in their own work.

This tutorial will be *hands-on*, with breaks for exercises;
participants are strongly encouraged to bring a laptop running
Coq 8.1 (or a later release) and either Proof General or CoqIDE.

Tutorial topics

   - Defining language semantics in Coq
      - Abstract syntax
      - Inductively-defined relations
      - Derivations
   - Proving simple results
      - Fundamental tactics
      - Automation
      - Forward and backward reasoning
   - Scaling up to POPLmark
      - Semantic functions and conversion
      - Sets and environments
   - Representing binding
      - Locally nameless representation
      - Freshness through cofinite quantification
      - Syntactic type soundness

Registration will be through the POPL 2008 registration site:
     http://www.regmaster.com/conf/popl2008.html

The tutorial is organized and presented by members of the University of
Pennsylvania PLClub: Brian Aydemir, Aaron Bohannon, Benjamin Pierce,
Jeffrey Vaughan, Dimitrios Vytiniotis, Stephanie Weirich, and
Steve Zdancewic.

Questions can be sent to Stephanie Weirich (sweirich at cis.upenn.edu).