TY - GEN
T1 - Executable Semantics and Type Checking for Session-Based Concurrency in Maude
AU - Ramírez Restrepo, Carlos Alberto
AU - Pérez, Jorge A.
N1 - Publisher Copyright:
© 2022, Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - Session types are a well-established approach to communication correctness in message-passing programs. We present an executable specification of the operational semantics of a session-typed π -calculus, implemented in the Maude system. We also develop an executable specification of its associated algorithmic type checking, and describe how both specifications can be integrated. We further explore how our executable specification enables us to detect well-typed but deadlocked processes by leveraging reachability and model checking tools in Maude. Our developments define a promising new approach to the (semi)automated analysis of communication correctness in message-passing concurrency.
AB - Session types are a well-established approach to communication correctness in message-passing programs. We present an executable specification of the operational semantics of a session-typed π -calculus, implemented in the Maude system. We also develop an executable specification of its associated algorithmic type checking, and describe how both specifications can be integrated. We further explore how our executable specification enables us to detect well-typed but deadlocked processes by leveraging reachability and model checking tools in Maude. Our developments define a promising new approach to the (semi)automated analysis of communication correctness in message-passing concurrency.
UR - http://www.scopus.com/inward/record.url?scp=85135821684&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-12441-9_12
DO - 10.1007/978-3-031-12441-9_12
M3 - Conference contribution
AN - SCOPUS:85135821684
SN - 9783031124402
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 230
EP - 250
BT - Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
A2 - Bae, Kyungmin
PB - Springer Science and Business Media Deutschland GmbH
T2 - 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Y2 - 2 April 2022 through 3 April 2022
ER -