[TYPES/announce] Call for abstracts: Workshop on Mechanizing Metatheory

[Benjamin Pierce]

               ACM SIGPLAN Workshop on Mechanizing Metatheory

                             25 September, 2010
                            Baltimore, Maryland
                          (Co-located with ICFP'10)

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

                     Submission deadline: 21 July, 2010


SPECIAL 5TH ANNIVERSARY PROGRAM

    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. The goal of the WMM
    workshops is to bring researchers who are (or would like to be) using
    automated proof assistants for programming language metatheory
    together with developers of proof assistants with an interest in
    supporting research in programming languages.

    This WMM is an occasion to look back at five years of intensive effort
    on formalizing programming languages. The centerpiece of the event
    will be a series of invited talks in which major players in the area
    look both back and forward, offering their perspectives on what has
    been achieved and what challenges remain.

    There will also be a session of short contributed presentations by
    workshop participants, selected from submitted abstracts.

    Invited Speakers

     * Andrew Appel, Princeton University
     * Karl Crary, Carnegie Mellon University
     * Amy Felty, University of Ottawa
     * Christian Urban, TU Munich
     * Steve Zdancewic, University of Pennsylvania


CALL FOR ABSTRACTS

  Important Dates

   * Submission deadline for abstracts: 21 July, 2010
   * Author Notification: 15 August, 2010
   * Workshop: Saturday, 25 September, 2010

  Scope

   * Tool demonstrations: proof assistants, logical frameworks,
     visualizers, etc.
   * Libraries for programming language metatheory
   * Novel formalization techniques
   * Investigation of formalization issues, especially with respect to
     variable binding
   * Examples of formalized programming language metatheory
   * Analysis and comparison of solutions to the POPLmark challenge
   * Proposals for new challenge problems that benchmark programming
     language work