POPL 2018 (series) / CoqPL 2018 (series) / The Fourth International Workshop on Coq for Programming Languages /
A calculus for logical refinements in separation logic
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.
(FruminKrebbers-CoqPL18.pdf) | 617KiB |
(Frumin-Krebbers-CoqPL18-Slides.pdf) | 366KiB |
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
Sat 13 Jan
Displayed time zone: Tijuana, Baja California change
16:00 - 18:05 | |||
16:00 25mTalk | 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 25mTalk | Revisiting Parametricity: Inductives and Uniformity of Propositions CoqPL File Attached | ||
16:50 25mTalk | Towards Context-Aware Data Refinement CoqPL Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue University File Attached | ||
17:15 25mTalk | Mechanizing the Construction and Rewriting of Proper Functions in Coq CoqPL Edwin Westbrook Galois, Inc. File Attached | ||
17:40 25mTalk | A calculus for logical refinements in separation logic CoqPL File Attached |