[isabelle] Workshop on Mechanizing Metatheory

     2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory

                          Freiburg, Germany

                       Sponsored by ACM SIGPLAN
                       Co-located with ICFP'07.


  Important Dates

     * Submission deadline: 18 June 2007
     * Author Notification: 16 July 2007
     * Workshop: 4 October 2007

  Workshop Description

   Researchers in programming languages have long felt the need for
   tools to help formalize and check their work. With advances in
   language technology demanding deep understanding of ever larger and
   more complex languages, this need has become urgent. There are a
   number of automated proof assistants being developed within the
   theorem proving community that seem ready or nearly ready to be
   applied in this domain--yet, despite numerous individual efforts in
   this direction, the use of proof assistants in programming language
   research is still not commonplace: the available tools are
   confusingly diverse, difficult to learn, inadequately documented,
   and lacking in specific library facilities required for work in
   programming languages.

   The goal of this workshop is to bring together researchers who have
   experience using automated proof assistants for programming
   language metatheory, and those who are interested in using tool
   support for formalizing their work. One starting point for
   discussion will be the obstacles that hinder mechanisation (whether
   they be pragmatic or technical), and what users and developers can
   do to overcome them.


   The workshop will consist of presentations by the participants,
   selected from submitted abstracts. It will focus on providing a
   fruitful environment for interaction and presentation of ongoing
   work.  Participants are invited to submit working notes, source
   files, and abstracts for distribution to the attendees, but as the
   workshop has no formal proceedings, contributions may still be
   submitted for publication elsewhere. (See the SIGPLAN republication
   policy for more details.)


   The scope of the workshop includes, but is not limited to:
     * Tool demonstrations: proof assistants, logical frameworks,
       visualizers, etc.
     * Libraries for programming language metatheory.
     * Formalization techniques, especially with respect to binding
     * Analysis and comparison of solutions to the POPLmark challenge.
     * Examples of formalized programming language metatheory.
     * Proposals for new challenge problems that benchmark programming
       language work.

  Submission Guidelines

   Email submissions to michael.norrish AT nicta.com.au. Submissions
   should be no longer than one page and in PDF (preferably) or
   Postscript that is interpretable by Ghostscript and printable on US
   Letter or A4 sized paper.

  Conference Organization

   Program Committee

          + Karl Crary, Carnegie Mellon University
          + Gerwin Klein, National ICT Australia
          + Michael Norrish, National ICT Australia (chair)
          + Randy Pollack, Edinburgh University
          + Steve Zdancewic, University of Pennsylvania

   Workshop Organizers

          + Benjamin Pierce, University of Pennsylvania
          + Stephanie Weirich, University of Pennsylvania

  Previous Workshops

     * Portland, 2006 (Colocated with ICFP)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.