The Fourth ACM SIGPLAN Workshop
Programming Languages meets Program Verification

Tuesday, January 19, 2010
Madrid, Spain
Affiliated with POPL 2010.

Overview: This will be the fourth ACM SIGPLAN Workshop on Programming Languages meets Program Verification.

The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic and/or structural properties of the programming language. One example is dependently typed programming languages, which leverage a language's type system to specify and check richer than usual specifications, possibly with programmer-provided proof terms. Another example is extended static checking systems like ESC/Java and Spec#, which incorporate pre- and postconditions along with a static verifier for these contracts.

Call for Papers

Registration: To register for PLPV'10, follow the link from the POPL 2010 page.


Invited Talk (9:00 - 10:00)

CertiCrypt: Formal Certification  of Code-Based Cryptographic Proofs
Gilles Barthe, Madrid Instutite for Advanced Studies

Session 1 (10:30 - 12:00)

Singleton types here, Singleton types there, Singleton types everywhere
Stefan Monnier and David Haguenauer

Operating system development with ATS
Matthew Danish and Hongwei Xi

Modular Reasoning about Invariants over Shared State with Interposed Data Members
Stephanie Balzer and Thomas Gross

Session 2 (2:00 - 3:00)

Resource Typing in Guru
Aaron Stump and Evan Austin

Free Theorems for Functional Logic Programs
Jan Christiansen, Daniel Seidel and Janis Voigtländer

Discussion (3:00 - 3:30)

Status update and discussion of the Trellys Project

Session 3 (4:00 - 5:00)

Arity-generic datatype-generic programming
Stephanie Weirich and Chris Casinghino

Challenge Benchmarks for Verification of Real-time Programs
Tomas Kalibera, Pavel Parizek, Ghaith Haddad, Gary T. Leavens, and Jan Vitek.

Co-Chairs Program Committee Previous PLPVs