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:
Steering Committee, 2011-2014.
- Thorsten Altenkirch, co-chair (The University of Nottingham)
- Cormac Flanagan, co-chair (The University of California, Santa Cruz)
- John Hughes (Chalmers University)
- Rustan Leino (Microsoft Research)
- Xavier Leroy (INRIA)
- Simon Peyton-Jones (Microsoft Research)
- Aaron Stump (The University of Iowa)
- Stephanie Weirich (The University of Pennsylvania)
Former Steering Committee, 2007-2010.
- Peter Dybjer (Chalmers University of Technology, Sweden)
- Conor McBride (The University of Strathclyde, UK)
- Simon Peyton-Jones (Microsoft Research Cambridge, UK)
- Tim Sheard (Portland State University, USA)
- Aaron Stump, co-chair (The University of Iowa, USA)
- Hongwei Xi, co-chair (Boston University, USA)