ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Thu 16 Apr 2015 14:30 - 15:00 at Skeel - Session 8 Chair(s): Jan Vitek

We propose an expressive type system with implicit coercions and both coherent and incoherent abstraction over coercions. This allows a fine-grained control of dependencies between computations and the logical hypotheses they depend on, while preserving the implicit use of hypotheses and restoring confluence. Combining implicit hypotheses and full reduction leads to a better understanding of GADTs, provides a better continuum between explicit and implicit type information, and would be a good setting for studying extraction of computational contents from proofs in proof assistants.

Thu 16 Apr
Times are displayed in time zone: Azores change

14:00 - 16:00
Session 8ESOP at Skeel
Chair(s): Jan VitekNortheastern University
14:00
30m
Talk
Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs
ESOP
Cristina DavidUniversity of Oxford, Daniel KroeningUniversity of Oxford, Matt LewisUniversity of Oxford
14:30
30m
Talk
Full reduction in the face of absurdity
ESOP
15:00
30m
Talk
CoLoSL: Concurrent Local Subjective Logic
ESOP
Azalea RaadImperial College London, Jules VillardImperial College London, Philippa GardnerImperial College London
15:30
30m
Talk
A Separation Logic for Fictional Sequential Consistency
ESOP
Filip SieczkowskiAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University, Jean Pichon-PharabodUniversity of Cambridge