Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.

[Caml-list] Coq Tutorial at POPL 2008: Using Proof Assistants for Programming Language Research

Skip to first unread message

Stephanie Weirich

Nov 20, 2007, 3:22:32 PM11/20/07
to,,, Haskell List,

Tutorial Announcement and Call for Participation

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

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


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

This tutorial will be tailored to people who are familiar with syntactic
proofs of programming language metatheory (type soundness, etc.), but
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

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
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:

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

Questions can be sent to Stephanie Weirich (

Caml-list mailing list. Subscription management:
Beginner's list:
Bug reports:

0 new messages