PLPV 2013

The Seventh ACM SIGPLAN Workshop on
Programming Languages meets Program Verification 

22nd January, 2013
Rome, Italy
(Affiliated with POPL 2013)


The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification, by bringing together experts from diverse areas like types, contracts, interactive theorem proving, model checking and program analysis. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic or structural properties of the programming language. One example are dependently typed programming languages, which leverage a language's type system to specify and check rich specifications. Another example are extended static checking systems which incorporate contracts with either static or dynamic contract checking.

Program (print version)

08:00am Breakfast

09:00am Session 1: Verification of Programming Languages
(Chair: Andreas Abel)

   Modular Type-Safety Proofs in Agda
   Christopher Schwaab and Jeremy Siek

   Compiling Contextual Objects: Bringing Higher-Order Abstract Syntax to Programmers
   Francisco Ferreira, Brigitte Pientka and Stefan Monnier

10:00am Coffee

10:30am Session 2: Invited talk on Dependently Typed Programming
(Chair: Tim Sheard)

   Idris: General Purpose Programming with Dependent Types (Abstract)
   Edwin Brady, University of St. Andrews, Scotland

12:00pm Lunch

02:30pm Session 3: Complexity and Security
(Chair: Chung-Kil Hur)

   A Static Cost Analysis for a Higher-Order Language
   Norman Danner, Jennifer Paykin and James Royer

   Towards Formal Verification of TLS Network Packet Processing in C
   Reynald Affeldt and Nicolas Marti

   Automated Analysis of Rule-Based Access Control Policie
   Clara Bertolissi and Worachet Uttha

04:00pm Coffee

04:30pm Session 4: Functional Reactive Programming
(Chair: Brigitte Pientka)

   Causality For Free!
         Parametricity Implies Causality for Functional Reactive Programs

   Alan Jeffrey

   Temporal Logic with “Until”:
         Functional Reactive Programming with Processes and Concrete Process Categories

   Wolfgang Jeltsch

05:30pm End

The proceedings are available in the ACM digital library.

Student Attendees
Students with accepted papers or posters are encouraged to apply for a SIGPLAN PAC grant that will help to cover travel expenses to PLPV. Details on the PAC program and the application can be found here.

Program Committee

Call for Papers

Previous PLPVs