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 AprDisplayed time zone: Azores change
Thu 16 Apr
Displayed time zone: Azores change
14:00 - 16:00 | |||
14:00 30mTalk | Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs ESOP Cristina David University of Oxford, Daniel Kroening University of Oxford, Matt Lewis University of Oxford | ||
14:30 30mTalk | Full reduction in the face of absurdity ESOP | ||
15:00 30mTalk | CoLoSL: Concurrent Local Subjective Logic ESOP Azalea Raad Imperial College London, Jules Villard Imperial College London, Philippa Gardner Imperial College London | ||
15:30 30mTalk | A Separation Logic for Fictional Sequential Consistency ESOP Filip Sieczkowski Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University, Jean Pichon-Pharabod University of Cambridge |