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.
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
Idris is a general purpose pure
functional programming language with dependent types. Its syntax is
influenced by Haskell and its features include full dependent types
and records, type classes, tactic based theorem proving, totality
checking and an optimising compiler with a foreign function interface.
One of the goals of the Idris project is to bring type-based program
verification techniques to functional programmers while still
supporting efficient systems programming via an optimising compiler
and interaction with external libraries. In this talk I will introduce
dependently typed programming using Idris, and demonstrate its
features using several examples including an interpreter for the
simply typed lambda calculus, and a verified binary adder. I will
also show how the Idris compiler generates executable code, maintaining
a phase distinction between compile-time and run-time terms.
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.