ITU

Machine-Checked Semantic Session Typing

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

Standard

Machine-Checked Semantic Session Typing. / Hinrichsen, Jonas Kastberg; Louwrink, Daniël; Krebbers, Robbert; Bengtson, Jesper.

CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, 2021. p. 178–198.

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

Harvard

Hinrichsen, JK, Louwrink, D, Krebbers, R & Bengtson, J 2021, Machine-Checked Semantic Session Typing. in CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, pp. 178–198. https://doi.org/10.1145/3437992.3439914

APA

Hinrichsen, J. K., Louwrink, D., Krebbers, R., & Bengtson, J. (2021). Machine-Checked Semantic Session Typing. In CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 178–198). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439914

Vancouver

Hinrichsen JK, Louwrink D, Krebbers R, Bengtson J. Machine-Checked Semantic Session Typing. In CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery. 2021. p. 178–198 https://doi.org/10.1145/3437992.3439914

Author

Hinrichsen, Jonas Kastberg ; Louwrink, Daniël ; Krebbers, Robbert ; Bengtson, Jesper. / Machine-Checked Semantic Session Typing. CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, 2021. pp. 178–198

Bibtex

@inproceedings{618f45a050de43b2a610fe8b52212bdd,
title = "Machine-Checked Semantic Session Typing",
abstract = "Session types—a family of type systems for message-passing concurrency—have been subject to many extensions, where each extension comes with a separate proof of type safety. These extensions cannot be readily combined, and their proofs of type safety are generally not machine checked, making their correctness less trustworthy. We overcome these shortcomings with a semantic approach to binary asynchronous affine session types, by developing a logical relations model in Coq using the Iris program logic. We demonstrate the power of our approach by combining various forms of polymorphism and recursion, asynchronous subtyping, references, and locks/mutexes. As an additional benefit of the semantic approach, we demonstrate how to manually prove typing judgements of racy, but safe, programs that cannot be type checked using only the rules of the type system.",
keywords = "Message passing, Session types, Separation logic, Semantic typing, Iris, Coq",
author = "Hinrichsen, {Jonas Kastberg} and Dani{\"e}l Louwrink and Robbert Krebbers and Jesper Bengtson",
year = "2021",
doi = "10.1145/3437992.3439914",
language = "English",
pages = "178–198",
booktitle = "CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs",
publisher = "Association for Computing Machinery",
address = "United States",

}

RIS

TY - GEN

T1 - Machine-Checked Semantic Session Typing

AU - Hinrichsen, Jonas Kastberg

AU - Louwrink, Daniël

AU - Krebbers, Robbert

AU - Bengtson, Jesper

PY - 2021

Y1 - 2021

N2 - Session types—a family of type systems for message-passing concurrency—have been subject to many extensions, where each extension comes with a separate proof of type safety. These extensions cannot be readily combined, and their proofs of type safety are generally not machine checked, making their correctness less trustworthy. We overcome these shortcomings with a semantic approach to binary asynchronous affine session types, by developing a logical relations model in Coq using the Iris program logic. We demonstrate the power of our approach by combining various forms of polymorphism and recursion, asynchronous subtyping, references, and locks/mutexes. As an additional benefit of the semantic approach, we demonstrate how to manually prove typing judgements of racy, but safe, programs that cannot be type checked using only the rules of the type system.

AB - Session types—a family of type systems for message-passing concurrency—have been subject to many extensions, where each extension comes with a separate proof of type safety. These extensions cannot be readily combined, and their proofs of type safety are generally not machine checked, making their correctness less trustworthy. We overcome these shortcomings with a semantic approach to binary asynchronous affine session types, by developing a logical relations model in Coq using the Iris program logic. We demonstrate the power of our approach by combining various forms of polymorphism and recursion, asynchronous subtyping, references, and locks/mutexes. As an additional benefit of the semantic approach, we demonstrate how to manually prove typing judgements of racy, but safe, programs that cannot be type checked using only the rules of the type system.

KW - Message passing

KW - Session types

KW - Separation logic

KW - Semantic typing

KW - Iris

KW - Coq

U2 - 10.1145/3437992.3439914

DO - 10.1145/3437992.3439914

M3 - Article in proceedings

SP - 178

EP - 198

BT - CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

PB - Association for Computing Machinery

ER -

ID: 85825613