Email Gateway (Aug 18 2022 at 10:09): Email Gateway (Aug 18 2022 at 10:09):From: Michael Norrish <michael.norrish@nicta.com.au>
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)
Last updated: May 03 2024 at 12:27 UTC