TY - GEN
T1 - A higher-order logic for concurrent termination-preserving refinement
AU - Tassarotti, Joseph
AU - Jung, Ralf
AU - Harper, Robert
N1 - 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 -