[TYPES/announce] CFP for PLPV 2007

[Hongwei Xi]

Call For Papers:

Programming Languages meets Program Verification (PLPV) 2007

A workshop affiliated with ICFP 2007

Date: October 5th, 2007

URL: http://www.plpv.org

*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.  In some cases, this is done by designing the
programming language to facilitate program verification, possibly
through an expressive type system.  In other cases, tighter integration
is achieved by exporting more statically computed semantic information
from the program to an external verification engine or environment.  In
all cases, the motivation is to reduce the burden of program
verification by taking greater advantage of static 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.

    -- improving performance or quality of verification algorithms using
       richer semantic information (like type information) about the
       program.

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

    -- meta-theoretic properties of languages for programming with
       proofs or other evidential artifacts.

*Submissions*. Submissions should be prepared with <a
href="http://www.acm.org/sigs/sigplan/authorInformation.htm">ACM SIGPLAN
two-column conference format</a> and fall into one of the following three
categories:

(1) 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
    publication).

(2) Experience reports (at most 6 pages in total length).
    Submissions in this category should report on interesting
    worked examples as well as practical insights.  They should
    focus on experience gained during implementation (and not
    on theoretical results).

(3) Proposals for challenge problems (at most 6 pages in total length).
    Submissions in this category should describe an application problem,
    for which language-based program verification techniques could be
    applied to establish correctness.  The application should be of
    appropriate size and complexity to serve as a challenge problem
    (with, for example, Microsoft Office being too large and merge-sort
    too small).  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*.

    -- Electronic submission: June 15.
    -- Notification: July 13.
    -- Final version: August 3. 
    -- Workshop: October 5.

*Invited Speaker*: TBA

*Organizers*.

    -- Aaron Stump (Washington University in St. Louis)
    -- Hongwei Xi (Boston University) 

*Program Committee*.

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