Sat 13 Jan 2018 17:40 - 18:05 at Watercourt A - Semantics and Synthesis Chair(s): Ilya Sergey

We present a formalization of logical refinements of programs in a higher-order programming languages with general references, polymorphism and existential types, and concurrency. The logical refinement is sound w.r.t. contextual refinements of programs, and has been formalized in Coq, together with a number of case studies, in state of the art concurrent separation logic Iris. The work extends on the initial interpretation of logical relations in Iris by Krebbers et al., to the extent that we provide a calculus that allows one to reason about logical refinement in an abstract way, together with a collection of Coq tactics that make reasoning in the calculus tractable for realistic examples.

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

16:00 - 18:05
Semantics and SynthesisCoqPL at Watercourt A
Chair(s): Ilya Sergey University College London
16:00
25m
Talk
Phantom Types for Quantum Programs
CoqPL
Robert Rand University of Pennsylvania, Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of Pennsylvania
File Attached
16:25
25m
Talk
Revisiting Parametricity: Inductives and Uniformity of Propositions
CoqPL
Abhishek Anand Cornell University, Greg Morrisett Cornell University
File Attached
16:50
25m
Talk
Towards Context-Aware Data Refinement
CoqPL
Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue University
File Attached
17:15
25m
Talk
Mechanizing the Construction and Rewriting of Proper Functions in Coq
CoqPL
Edwin Westbrook Galois, Inc.
File Attached
17:40
25m
Talk
A calculus for logical refinements in separation logic
CoqPL
Dan Frumin Radboud University, Robbert Krebbers Delft University of Technology
File Attached