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:

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.