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 |