PLPV 2013

The Seventh ACM SIGPLAN Workshop on
Programming Languages meets Program Verification

22nd January, 2013

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
   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