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.
The workshop will consist of presentations by the
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
The scope of the workshop includes, but is not limited
- 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
- Examples of formalized programming language
- Proposals for new challenge problems that
benchmark programming language work