Programming Languages meets Program Verification (PLPV) 2007
October 5, 2007
Affiliated with ICFP 2007.
Proceedings online at the ACM Digital Library.
Workshop schedule (including unofficial copies of some of the papers).
Invited Speaker: Claude Marché (INRIA)
Topic. PLPV is concerned with
language-based approaches to program verification. These approaches
integrate programming language semantics and verification techniques
in a tighter way than is typically done in traditional verification.
An example is dependently typed programming, where types provide rich
specifications, and programs may contain proof terms to establish type
equivalences or satisfy pre-conditions. The motivation for this
approach is to reduce the burden of program verification by taking
greater advantage of semantic properties (like type properties) of the
program during verification.
Paper Topics. Research on language-based
approaches to program
correctness spans compilers, programming languages, and computational
logic. Possible paper topics include:
- practical programming with dependent types (possibly addressing
issues such as mutable state and other effectful constructs).
- extended static checking; type systems and other static analyses
relying on semantically rich program annotations.
- integration of theorem proving and programming environments.
- programming language constructs or methodologies where
artifacts are included solely to convince the type checker
that a piece of code is type safe (e.g., type representations,
- meta-theoretic properties of languages for programming with
proofs or other evidential artifacts.
- improving performance or quality of verification algorithms
using richer semantic information (like type information) about the
Submissions. Submissions should be
prepared with ACM
SIGPLAN two-column conference format. We request authors to
follow the "author-date" citation format which is being used by ICFP.
See the ICFP call for
papers for more information on this format. Submissions should
fall into one of the following three categories:
Online Submission. Electronic
submission of PDF files is now closed (EasyChair page for PLPV07).
- Regular research papers (at most 12 pages in total length).
Submissions in this category should describe new work on the above
or related topics (not currently submitted elsewhere for
- Work-in-progress reports (at most 6 pages in total length).
Submissions in this category need not report orignal
research. Instead, they are intended to inform others about
interesting and significant applications as well as insights gained
in the practice of combining programming with verification.
- Proposals for challenge problems (at most 6 pages in total length).
Submissions in this category should describe an application for
which the author believes language-based program verification
techniques can be applied to establish correctness. Preference
will be given to broadly used applications, and to ones where
correctness is of demonstrable importance (a crucial piece of
Internet infrastructure might be an example).
Review Process. Each submission will
receive three reviews. The PC members (except the co-chairs) may
submit either kind of paper. Reviewing (as well as submission) will be
managed using the EasyChair system, which prevents PC members from
accessing discussions of their own papers.
Publication. Accepted papers will be
published by the ACM and appear in the ACM digital library.
Important Dates (finalized).
- Electronic submission: June 15.
- Notification: July 13.
- Final version: August 3.
- Workshop: October 5.
- Aaron Stump (Washington University in St. Louis)
- Hongwei Xi (Boston University)
- Peter Dybjer (Chalmers, Sweden)
- John Hughes (Chalmers, Sweden)
- Conor McBride (University of Nottingham, UK)
- Stefan Monnier (University of Montreal, Canada)
- Brigitte Pientka (McGill University, Canada)
- Francois Pottier (INRIA, France)
- Chung-chieh Shan (Rutgers, USA)
- Tim Sheard (Portland State University, USA)
- Aaron Stump, co-chair (Washington University in St. Louis, USA)
- Martin Sulzmann (NUS, Singapore)
- Walid Taha (Rice University, USA)
- Simon Thompson (University of Kent, UK)
- Hongwei Xi, co-chair (Boston University, USA)