[TYPES/announce] Workshop on Mechanizing Metatheory

[Michael Norrish]

      2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory

                           Freiburg, Germany

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

                http://www.cis.upenn.edu/~sweirich/wmm/

   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.

   Format

    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.)

   Scope

    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
        issues.
      * 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)