- Program Chairs:
- Nils Anders Danielsson,
- Bart Jacobs
- Sponsor:
- sigplan
Welcome to the 8th edition of Programming Languages meets Program Verification (PLPV).
The PLPV series of workshops aims to bring together researchers working in the intersection of programming languages and program verification. Relevant topics include, but are not limited to, types, contracts, interactive theorem proving, model checking, and program analysis. A common theme of work in this area is to make program verification easier through the use and/or design of programming language features. One example is provided by dependent types, which make it possible to specify and verify complicated properties using a language's type system. Another example is the combination of programming languages with SMT solvers to automate program verification.
This year the workshop received seven submissions, out of which five were accepted for publication. The programme also includes two invited talks, one by Ranjit Jhala, and one by Lee Pike.
Proceeding Downloads
Programming languages for high-assurance autonomous vehicles: extended abstract
We briefly describe the use of embedded domain-specific languages to improve programmer productivity and increase software assurance in the context of building a fully-featured autopilot for unpiloted aircraft.
The recursive polarized dual calculus
This paper introduces the Recursive Polarized Dual Calculus (RP-DC), based on Wadler's Dual Calculus. RP-DC features a polarized form of reduction, which enables several simplifications over previous related systems. It also adds inductive types with ...
Substructural typestates
Finding simple, yet expressive, verification techniques to reason about both aliasing and mutable state has been a major challenge for static program verification. One such approach, of practical relevance, is centered around a lightweight typing ...
Refinement types for Haskell
We present LiquidHaskell (http://goto.ucsd.edu/liquid), an automatic verifier for Haskell. LiquidHaskell uses Refinement types, a restricted form of dependent types where relationships between values are encoded by decorating types with logical ...
Verified programs with binders
Programs that treat datatypes with binders, such as theorem provers or higher-order compilers, are regularly used for mission-critical purposes, and must be both reliable and performant. Formally proving such programs using as much automation as ...
Formalizing a correctness property of a type-directed partial evaluator
This paper presents our experience of formalizing Danvy's type-directed partial evaluator (TDPE) for the call-by-name lambda calculus in the proof assistant Coq. Following the previous approach by Coquand and Ilik, we characterize TDPE as a composition ...
An abstract categorical semantics for functional reactive programming with processes
Linear-time temporal logic and functional reactive programming (FRP) are related via a Curry-Howard correspondence. Thereby proofs of "always," "eventually," and "until" propositions correspond to behaviors, events, and processes, respectively. ...
Index Terms
- Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program Verification