Programming Languages meets Program Verification (PLPV) 2006
A workshop affiliated with IJCAR
2006, a FLoC conference.
Seattle, Washington
August 21, 2006
Preproceedings are here.
The FLoC page for PLPV '06 is here.
Motivation. While the essential ideas
of program verification have been understood for decades, the
practical ability to develop and maintain correct software at a
reasonable cost has remained elusive. Approaches based on manually
proving extracted verification conditions are often viewed as brittle
and burdensome, despite continued advances. Mostly automatic
techniques like static analysis and model checking face challenges
scaling to rich properties of large systems. Yet, as societies become
increasingly dependent on software systems, the need for a practical
way to build provably correct software has never been greater.
PL and Verification. Recent work is
exploring alternative, language-based approaches to program
verification. In these approaches, the programming language provides
mechanisms which allow the programmer to express, in some way, her
knowledge of why her code meets its specification. This knowledge is
connected more intimately to the code than is usually the case for
theorem proving approaches. One commonly used mechanism is dependent
types. Specifications are expressed as types, and the programming
language allows proofs of those specifications to be expressed as
terms inhabiting those types. Pre- and post-conditions of functions
are recorded in their input and return types, and the functions
require and produce proofs of those conditions as additional inputs
and outputs. One exciting possibility is that languages for
programming with proofs may enable developers to target a "continuum
of correctness," through varying amounts of effort on specification
and 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.
- 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,
equality types, certain uses of Haskell type classes).
- meta-theoretic properties of languages for programming with
proofs or other evidential artifacts.
- formal reasoning about mutable state, including separation logic.
Submissions. Submissions should
either be new research papers, prepared with article format in LaTeX,
between 12 and 18 pages in length (not counting appendices, which
reviewers will not be asked to review); or else position papers, same
format, of no more than 5 pages. Research papers describing
preliminary results or work in progress are very welcome. More time
for presentation at the workshop may be allotted for a full paper than
a position paper. Electronic submission of PostScript or PDF files
should be done via the EasyChair page for PLPV.
Review Process. Each submission will
receive three reviews. The co-chairs will limit themselves to
position papers, while other PC members 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. The proceedings of the
workshop will most likely be archived using ENTCS or as a technical
report (online) at one of the organizers' institutions.
Important Dates.
- Electronic submission: May 19.
- Notification: June 30.
- Final version: July 21.
Invited Speaker: Peter Dybjer
Organizers.
- Aaron Stump (Washington University in St. Louis)
- Hongwei Xi (Boston University)
Program Committee.
- Thorsten Altenkirch (University of Nottingham)
- Hugo Herbelin (Ecole Polytechnique)
- Simon Peyton-Jones (Microsoft Research)
- Randy Pollack (University of Edinburgh)
- Carsten Schuermann (IT University of Copenhagen)
- Zhong Shao (Yale University)
- Tim Sheard (Portland State University)
- Aaron Stump, co-chair (Washington University in St. Louis)
- Hongwei Xi, co-chair (Boston University)