Programming Languages meets Program Verification (PLPV)

Topic. The PLPV workshop 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.

Meetings of PLPV:

• PLPV 2009 (affiliated with POPL 2009).
• PLPV 2007 (affiliated with ICFP 2007).
• PLPV 2006 (affiliated with IJCAR 2006).

Steering Committee.

• Peter Dybjer (Chalmers University of Technology, Sweden)
• Conor McBride (University of Nottingham, UK)
• Simon Peyton Jones (Microsoft Research Cambridge, UK)
• Tim Sheard (Portland State University, USA)
• Aaron Stump, co-chair (Washington University in St. Louis, USA)
• Hongwei Xi, co-chair (Boston University, USA)