Slot Chair
Tue 14:00--14:10 Peter Thiemann Welcome
14:10--15:30 Didier Rémy Session "Types":
Andreas Abel:
Coinductive programming with copatterns

Wouter Swierstra:
Auto in Agda

Atsushi Igarashi:
A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers

Ranjit Jhala:
Bounded Refinement Types
Break
16:00--17:20 Anders Møller Session "Program analysis"
Matthew Fluet:
Type- and Control-Flow Analysis

Christian Hammer:
Declassification in the Browser

Francesco Ranzato:
Analysing Completeness in Program Analysis

Joshua Dunfield:
Evaluation-order Polymorphism
Wed 9:00--10:30 Klaus Ostermann Session "Concurrency"
Ivan Lanese:
Reversible Concurrent Systems

Ilya Sergey:
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects

Vasco Vasconcelos:
Protocol-based Verification of Message-passing Parallel Programs
11:00--12:20 Ranjit Jhala Session "Verification"
Arthur Charguéraud:
Machine-checked verification of amortized complexity analyses

Dominique Devriese:
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity

Sophia Drossopoulou:
Reasoning about Programs in the Presence of Code of Unknown Provenance

Keiko Nakata:
Formal Verification of a Microkernel at FireEye
Lunchbreak
14:00--15:00 Christian Hammer Session "Objects"
James Noble:
On Grace

Anders Møller:
Message Safety in Dart

Klaus Ostermann:
Automatic Refunctionalization
Break
15:30--16:30 Andreas Abel Session "Functional Programming"
Didier Rémy:
Full Reduction and GADTs

Peter Thiemann:
Derivatives in Program Analysis

Jeremy Siek:
A Tracing JIT for a Functional Language
16:30--16:45 Peter Thiemann Closing