[TYPES/announce] Workshop on Mechanizing Metatheory
Stephanie Weirich
sweirich at cis.upenn.edu
Tue Jan 10 09:12:51 EST 2006
1st ACM SIGPLAN Workshop on Mechanizing Metatheory
Portland, Oregon, USA
Co-located with ICFP'06. Exact date TBA.
Important Dates
Submission deadline: June 3, 2006
Author Notification: July 1, 2006
Workshop: TBA
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
POPLmark challenge: a set of challenge problems intended to assess the
state of the art in this area. More information about the POPLmark
challenge is available from http://www.cis.upenn.edu/proj/plclub/mmm.
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 http://www.acm.org/sigs/sigplan/republicationpolicy.htm)
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
The deadline for submissions of abstracts is June 3, 2006. Email
submissions to sweirich AT cis.upenn.edu. 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.
Program Committee
Karl Crary, Carnegie Mellon University
Xavier Leroy, INRIA Rocquencourt
Peter Sewell, Cambridge University
Michael Norrish, Canberra Research Lab, National ICT Australia
Stephanie Weirich, University of Pennsylvania (chair)
Workshop Organizers
Benjamin Pierce, University of Pennsylvania
Stephanie Weirich, University of Pennsylvania
Steve Zdancewic, University of Pennsylvania
More information about the Types-announce
mailing list