[TYPES/announce] Programming Languages meets Program Verification: CFP

[Aaron Stump]

Call For Papers:

Programming Languages meets Program Verification (PLPV) 2006

A workshop affiliated with IJCAR 2006, a FLoC conference.
Seattle, Washington, USA
August 21, 2006

http://cl.cse.wustl.edu/plpv06/

*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 (see the
PLPV web page).

*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 be archived in ENTCS.

*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)