Email Gateway (Aug 18 2022 at 12:57): Email Gateway (Aug 18 2022 at 12:57):From: Stephanie Weirich <sweirich@cis.upenn.edu>
Journal of Automated Reasoning
Special issue on the POPLmark Challenge
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
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
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 June 15, 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.
For more information, see
http://www.seas.upenn.edu/~sweirich/jar-poplmark/
Guest Editors
Stephanie Weirich, University of Pennsylvania
Benjamin Pierce, University of Pennsylvania
Email Gateway (Aug 18 2022 at 13:31):From: Stephanie Weirich <sweirich@cis.upenn.edu>
[Note: The deadline for this special issue has been extended
to June 29, 2009. Please do submit a paper. --Stephanie]
Journal of Automated Reasoning
Special issue on the POPLmark Challenge
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
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
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 June 29, 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.
For more information, see
http://www.seas.upenn.edu/~sweirich/jar-poplmark/
Guest Editors
Stephanie Weirich, University of Pennsylvania
Benjamin Pierce, University of Pennsylvania
Last updated: May 03 2024 at 12:27 UTC