ITU

Actris: session-type based reasoning in separation logic

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Standard

Actris: session-type based reasoning in separation logic. / Hinrichsen, Jonas Kastberg; Bengtson, Jesper; Krebbers, Robbert.

Proceedings of the ACM on Programming Languages. ed. / Philip Wadler. Vol. 4 Association for Computing Machinery, 2020. p. 6:1 6.

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Harvard

Hinrichsen, JK, Bengtson, J & Krebbers, R 2020, Actris: session-type based reasoning in separation logic. in P Wadler (ed.), Proceedings of the ACM on Programming Languages. vol. 4, 6, Association for Computing Machinery, pp. 6:1. https://doi.org/10.1145/3371074

APA

Hinrichsen, J. K., Bengtson, J., & Krebbers, R. (2020). Actris: session-type based reasoning in separation logic. In P. Wadler (Ed.), Proceedings of the ACM on Programming Languages (Vol. 4, pp. 6:1). [6] Association for Computing Machinery. https://doi.org/10.1145/3371074

Vancouver

Hinrichsen JK, Bengtson J, Krebbers R. Actris: session-type based reasoning in separation logic. In Wadler P, editor, Proceedings of the ACM on Programming Languages. Vol. 4. Association for Computing Machinery. 2020. p. 6:1. 6 https://doi.org/10.1145/3371074

Author

Hinrichsen, Jonas Kastberg ; Bengtson, Jesper ; Krebbers, Robbert. / Actris: session-type based reasoning in separation logic. Proceedings of the ACM on Programming Languages. editor / Philip Wadler. Vol. 4 Association for Computing Machinery, 2020. pp. 6:1

Bibtex

@inproceedings{475db6ac7a504f018c051a7e17de8d63,
title = "Actris: session-type based reasoning in separation logic",
abstract = "Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however,it is often combined with other programming and concurrency paradigms, such as higher-order functions,mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functionalcorrectness of programs that use a combination of the aforementioned features. Actris combines the powerof modern concurrent separation logics with a first-class protocol mechanism—based on session types—forreasoning about message passing in the presence of other concurrency paradigms. We show that Actrisprovides a suitable level of abstraction by proving functional correctness of a variety of examples, including adistributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, usingrelatively simple specifications. Soundness of Actris is proved using a model of its protocol mechanism in theIris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs,as well as all examples in the paper, in the Coq proof assistant",
author = "Hinrichsen, {Jonas Kastberg} and Jesper Bengtson and Robbert Krebbers",
year = "2020",
doi = "10.1145/3371074",
language = "English",
volume = "4",
pages = "6:1",
editor = "Philip Wadler",
booktitle = "Proceedings of the ACM on Programming Languages",
publisher = "Association for Computing Machinery",
address = "United States",

}

RIS

TY - GEN

T1 - Actris: session-type based reasoning in separation logic

AU - Hinrichsen, Jonas Kastberg

AU - Bengtson, Jesper

AU - Krebbers, Robbert

PY - 2020

Y1 - 2020

N2 - Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however,it is often combined with other programming and concurrency paradigms, such as higher-order functions,mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functionalcorrectness of programs that use a combination of the aforementioned features. Actris combines the powerof modern concurrent separation logics with a first-class protocol mechanism—based on session types—forreasoning about message passing in the presence of other concurrency paradigms. We show that Actrisprovides a suitable level of abstraction by proving functional correctness of a variety of examples, including adistributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, usingrelatively simple specifications. Soundness of Actris is proved using a model of its protocol mechanism in theIris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs,as well as all examples in the paper, in the Coq proof assistant

AB - Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however,it is often combined with other programming and concurrency paradigms, such as higher-order functions,mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functionalcorrectness of programs that use a combination of the aforementioned features. Actris combines the powerof modern concurrent separation logics with a first-class protocol mechanism—based on session types—forreasoning about message passing in the presence of other concurrency paradigms. We show that Actrisprovides a suitable level of abstraction by proving functional correctness of a variety of examples, including adistributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, usingrelatively simple specifications. Soundness of Actris is proved using a model of its protocol mechanism in theIris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs,as well as all examples in the paper, in the Coq proof assistant

U2 - 10.1145/3371074

DO - 10.1145/3371074

M3 - Article in proceedings

VL - 4

SP - 6:1

BT - Proceedings of the ACM on Programming Languages

A2 - Wadler, Philip

PB - Association for Computing Machinery

ER -

ID: 85391054