Executable Semantics and Type Checking for Session-Based Concurrency in Maude

Carlos Alberto Ramírez Restrepo; Jorge A. Pérez

doi:10.1007/978-3-031-12441-9_12

Executable Semantics and Type Checking for Session-Based Concurrency in Maude

Carlos Alberto Ramírez Restrepo, Jorge A. Pérez

Department of Electronics and Computer Science

University of Groningen

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

1 Scopus citations

Abstract

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.

Original language	English
Title of host publication	Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
Editors	Kyungmin Bae
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	230-250
Number of pages	21
ISBN (Print)	9783031124402
DOIs	https://doi.org/10.1007/978-3-031-12441-9_12
State	Published - 2022
Event	14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 - Munich, Germany Duration: 02 Apr 2022 → 03 Apr 2022

Publication series

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

Conference

Conference	14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Country/Territory	Germany
City	Munich
Period	02/04/22 → 03/04/22

Access to Document

10.1007/978-3-031-12441-9_12

Cite this

Ramírez Restrepo, C. A., & Pérez, J. A. (2022). Executable Semantics and Type Checking for Session-Based Concurrency in Maude. In K. Bae (Ed.), Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers (pp. 230-250). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13252 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-12441-9_12

Ramírez Restrepo, Carlos Alberto ; Pérez, Jorge A. / Executable Semantics and Type Checking for Session-Based Concurrency in Maude. Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. editor / Kyungmin Bae. Springer Science and Business Media Deutschland GmbH, 2022. pp. 230-250 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1d0c3c4ccf4b4575811f3f107f1ea104,

title = "Executable Semantics and Type Checking for Session-Based Concurrency in Maude",

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

author = "{Ram{\'i}rez Restrepo}, {Carlos Alberto} and P{\'e}rez, {Jorge A.}",

note = "Publisher Copyright: {\textcopyright} 2022, Springer Nature Switzerland AG.; 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 ; Conference date: 02-04-2022 Through 03-04-2022",

year = "2022",

doi = "10.1007/978-3-031-12441-9_12",

language = "English",

isbn = "9783031124402",

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

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "230--250",

editor = "Kyungmin Bae",

booktitle = "Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers",

address = "Germany",

}

Ramírez Restrepo, CA & Pérez, JA 2022, Executable Semantics and Type Checking for Session-Based Concurrency in Maude. in K Bae (ed.), Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13252 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 230-250, 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022, Munich, Germany, 02/04/22. https://doi.org/10.1007/978-3-031-12441-9_12

Executable Semantics and Type Checking for Session-Based Concurrency in Maude. / Ramírez Restrepo, Carlos Alberto; Pérez, Jorge A.
Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. ed. / Kyungmin Bae. Springer Science and Business Media Deutschland GmbH, 2022. p. 230-250 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13252 LNCS).

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

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.

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 -

Ramírez Restrepo CA, Pérez JA. Executable Semantics and Type Checking for Session-Based Concurrency in Maude. In Bae K, editor, Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. Springer Science and Business Media Deutschland GmbH. 2022. p. 230-250. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-12441-9_12