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
Times are displayed in time zone: Tijuana, Baja California change

16:00 - 18:05: Semantics and SynthesisCoqPL at Watercourt A
Chair(s): Ilya SergeyUniversity College London
16:00 - 16:25
Talk
CoqPL
Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
File Attached
16:25 - 16:50
Talk
CoqPL
Abhishek AnandCornell University, Greg MorrisettCornell University
File Attached
16:50 - 17:15
Talk
CoqPL
Paul KrogmeierPurdue University, Steven KiddPurdue University, Benjamin DelawarePurdue University
File Attached
17:15 - 17:40
Talk
CoqPL
Edwin WestbrookGalois, Inc.
File Attached
17:40 - 18:05
Talk
CoqPL
Dan FruminRadboud University, Robbert KrebbersDelft University of Technology
File Attached