From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 7744EBC69 for ; Tue, 20 Nov 2007 21:22:01 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAD/QQkfAXQImh2dsb2JhbACPFgEBAQgKKQ X-IronPort-AV: E=Sophos;i="4.21,443,1188770400"; d="scan'208";a="4449366" Received: from discorde.inria.fr ([192.93.2.38]) by mail2-smtp-roc.national.inria.fr with ESMTP; 20 Nov 2007 21:22:00 +0100 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id lAKKLFqm026947 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 20 Nov 2007 21:22:01 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAC/RQkeegkZPn2dsb2JhbACPFgEBAQEHBAYJIA X-IronPort-AV: E=Sophos;i="4.21,443,1188770400"; d="scan'208";a="6016261" Received: from stag.seas.upenn.edu ([158.130.70.79]) by mail3-smtp-sop.national.inria.fr with ESMTP; 20 Nov 2007 21:22:00 +0100 Received: from [158.130.50.184] (LVN510-1.cis.UPENN.EDU [158.130.50.184]) (authenticated bits=0) by stag.seas.upenn.edu (8.13.6/8.13.6) with ESMTP id lAKKLx3o017345 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NOT); Tue, 20 Nov 2007 15:21:59 -0500 Mime-Version: 1.0 (Apple Message framework v752.3) Content-Transfer-Encoding: 7bit Message-Id: Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: types-announce@lists.seas.upenn.edu, poplmark@lists.seas.upenn.edu, coq-club@pauillac.inria.fr, Haskell List , caml-list@inria.fr From: Stephanie Weirich Subject: Coq Tutorial at POPL 2008: Using Proof Assistants for Programming Language Research Date: Tue, 20 Nov 2007 15:21:57 -0500 X-Mailer: Apple Mail (2.752.3) X-Miltered: at discorde with ID 474341BB.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; weirich:01 coq:01 popl:01 popl:01 coq:01 co-located:01 sigplan:01 formalize:01 semantics:01 syntax:01 weirich:01 tailored:98 hands-on:98 tactics:98 abstract:01 ====================================================================== 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@cis.upenn.edu).