[TYPES/announce] Final 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 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