TY - GEN
T1 - A higher-order logic for concurrent termination-preserving refinement
AU - Tassarotti, Joseph
AU - Jung, Ralf
AU - Harper, Robert
N1 - Funding Information:
The authors thank Robbert Krebbers, Jeehoon Kang, Max Willsey, Frank Pfenning, Derek Dreyer, Lars Birkedal, and Jan Hoffmann for helpful discussions and feedback. This research was conducted with U.S. Government support under and awarded by DoD, Air Force Office of Scientific Research, National Defense Science and Engineering Graduate (NDSEG) Fellowship, 32 CFR 168a; and with support by a European Research Council (ERC) Consolidator Grant for the project “RustBelt”, funded under the European Union’s Horizon 2020 Framework Programme (grant agreement no. 683289). Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of these funding agencies.
Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.
PY - 2017
Y1 - 2017
N2 - Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a 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.
AB - Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a 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.
UR - http://www.scopus.com/inward/record.url?scp=85018699953&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85018699953&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-54434-1_34
DO - 10.1007/978-3-662-54434-1_34
M3 - Conference contribution
AN - SCOPUS:85018699953
SN - 9783662544334
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 909
EP - 936
BT - Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
A2 - Yang, Hongseok
PB - Springer Verlag
T2 - 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Y2 - 22 April 2017 through 29 April 2017
ER -