A Higher-Order Logic for Concurrent Termination-Preserving Refinement
J. Tassarotti, R. Jung, R. Harper.
Abstract:
Compiler correctness proofs for higher-order concurrent languages are
difficult: they involve establishing a termination-preserving
refinement between a \emph{concurrent} high-level source language and
an implementation that uses low-level shared memory primitives.
However, existing logics for proving concurrent refinement
either neglect properties such as termination, or only handle
first-order state. In this paper, we address these limitations by
extending Iris, a recent higher-order concurrent separation logic,
with support for reasoning about termination-preserving refinements.
To demonstrate the power of these extensions, we prove the correctness of an efficient
implementation of a higher-order, session-typed language. To our
knowledge, this is the first program logic capable of giving a
compiler correctness proof for such a language. The soundness of our
extensions and our compiler correctness proof have been mechanized in
Coq.