Journal of Automated Reasoning

Special Issue on the POPLmark Challenge

 Home · Call for papers (TXT) 

Call for papers

How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike? One crucial step towards achieving these goals is mechanized reasoning about language metatheory. 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.

In 2005, a group of programming language researchers at Penn and Cambridge issued "The POPLmark challenge": a set of challenge problems aimed at the programming language and theorem proving community to gauge progress in mechanizing programming language metatheory. The solutions to this challenge have been gathered at http://plclub.org/mmm/.

The goal of the special issue is a retrospective on the POPLmark challenge, summarizing and analyzing what has been learned. Submissions are encouraged, but not limited to, the following topics:

• 
  

* Complete, polished descriptions of specific POPLmark solutions,
   including well-commented proof scripts
* Analysis and comparison of solutions to the POPLmark challenge
* Descriptions and code for proof assistant extensions/libraries developed
   explicitly for the purpose of programming language metatheory
* New formalization techniques, especially with respect to binding issues

Submission details

• Proposals for new challenge problems that benchmark programming language work

Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.

Submissions are due July 6, 2009. We will keep a tight review schedule to enable publication of the special issue by mid 2010. Papers that do not progress through the reviewing cycle in a timely manner may be published in a later issue. Papers should be in pdf format following the JAR guidelines for authors. We encourage authors to keep their submissions below 30 pages. Authors should submit their papers electronically to sweirich@cis.upenn.edu.

Submission deadline

    June 29, 2009
    July 6, 2009

Guest Editors

• Stephanie Weirich,
  University of Pennsylvania
  
• Benjamin Pierce,
  University of Pennsylvania

 Maintained by sweirich@cis.upenn.edu | Design by Minimalistic Design