A higher-order logic for concurrent termination-preserving refinement

Joseph Tassarotti; Ralf Jung; Robert Harper

doi:10.1007/978-3-662-54434-1_34

A higher-order logic for concurrent termination-preserving refinement

Joseph Tassarotti, Ralf Jung, Robert Harper

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English (US)
Title of host publication	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
Editors	Hongseok Yang
Publisher	Springer Verlag
Pages	909-936
Number of pages	28
ISBN (Print)	9783662544334
DOIs	https://doi.org/10.1007/978-3-662-54434-1_34
State	Published - 2017
Event	26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 - Uppsala, Sweden Duration: Apr 22 2017 → Apr 29 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10201 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Country/Territory	Sweden
City	Uppsala
Period	4/22/17 → 4/29/17

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-662-54434-1_34

Cite this

Tassarotti, J., Jung, R., & Harper, R. (2017). A higher-order logic for concurrent termination-preserving refinement. In H. Yang (Ed.), 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 (pp. 909-936). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10201 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-54434-1_34

A higher-order logic for concurrent termination-preserving refinement. / Tassarotti, Joseph; Jung, Ralf; Harper, Robert.
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. ed. / Hongseok Yang. Springer Verlag, 2017. p. 909-936 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10201 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Tassarotti, J, Jung, R & Harper, R 2017, A higher-order logic for concurrent termination-preserving refinement. in H Yang (ed.), 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10201 LNCS, Springer Verlag, pp. 909-936, 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, 4/22/17. https://doi.org/10.1007/978-3-662-54434-1_34

Tassarotti J, Jung R, Harper R. A higher-order logic for concurrent termination-preserving refinement. In Yang H, editor, 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. Springer Verlag. 2017. p. 909-936. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-54434-1_34

Tassarotti, Joseph ; Jung, Ralf ; Harper, Robert. / A higher-order logic for concurrent termination-preserving refinement. 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. editor / Hongseok Yang. Springer Verlag, 2017. pp. 909-936 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7e4eb723eea34052bf380b4928486be9,

title = "A higher-order logic for concurrent termination-preserving refinement",

abstract = "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.",

author = "Joseph Tassarotti and Ralf Jung and Robert Harper",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag GmbH Germany 2017.; 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 ; Conference date: 22-04-2017 Through 29-04-2017",

year = "2017",

doi = "10.1007/978-3-662-54434-1_34",

language = "English (US)",

isbn = "9783662544334",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "909--936",

editor = "Hongseok Yang",

booktitle = "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",

}

TY - GEN

T1 - A higher-order logic for concurrent termination-preserving refinement

AU - Tassarotti, Joseph

AU - Jung, Ralf

AU - Harper, Robert

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 -

A higher-order logic for concurrent termination-preserving refinement

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this