[TYPES/announce] WMM'08 call for papers
Karl Crary
crary at cs.cmu.edu
Tue Apr 22 20:48:58 EDT 2008
Apologies for the cross-posting.
-----------------------------------------
Call for Papers
3rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory
Victoria, British Columbia, Canada
Sponsored by ACM SIGPLAN
Co-located with ICFP’08.
http://www.cis.upenn.edu/~sweirich/wmm/
Important Dates
* Submission deadline: 3 July 2008
* Author Notification: 1 August 2008
* Workshop: 20 September 2008
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 crary AT cs.cmu.edu. Submissions should be no
longer than one page and in PDF and printable on US Letter or A4 sized
paper. Persons for whom this poses a hardship should contact the program
chair.
Conference Organization
Program Committee
* Adam Chlipala, Jane Street Capital
* Karl Crary, Carnegie Mellon University (chair)
* Carsten Schuermann, IT University Copenhagen
* Aaron Stump, Washington University in St. Louis
* Christian Urban, TU Munich
Workshop Organizers
* Michael Norrish, National ICT Australia
* Stephanie Weirich, University of Pennsylvania
* Steve Zdancewic, University of Pennsylvania
Previous Workshops
* Freiburg, 2007
* Portland, 2006
More information about the Types-announce
mailing list