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

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