Programming Languages meets Program Verification (PLPV) 2007

Affiliated with ICFP 2007.

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, equality types).
• 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 program.

Submissions. Submissions should be new research papers, prepared with article format in LaTeX, of at most 15 pages in length (not counting appendices, which reviewers will not be asked to review). Research papers describing preliminary results or work in progress are preferred. Electronic submission of PostScript or PDF files will be done via the EasyChair system (a link will be provided here when the deadline is closer).

Review Process. Each submission will receive three reviews. The co-chairs will not submit papers, but the PC may submit papers. Reviewing will be managed using the EasyChair system, which prevents PC members from accessing discussions of their own papers.

Publication. PLPV is requesting publication of the workshop proceedings with ACM.

Important Dates.

• Electronic submission: May 15.
• Notification: July 8.
• Final version: August 1.

Invited Speaker: TBD

Organizers.

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

Program Committee.

• Peter Dybjer
• John Hughes
• Conor McBride
• Stefan Monnier
• Brigitte Pientka
• Francois Pottier
• Chung-chieh Shan
• Tim Sheard
• Aaron Stump (co-chair)
• Martin Sulzmann
• Walid Taha
• Simon Thompson
• Hongwei Xi (co-chair)

Previous PLPVs:

• PLPV 2006.