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

Producción: Capítulo del libro/informe/acta de congresoContribución a la conferenciarevisión exhaustiva

1 Cita (Scopus)

Resumen

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.

Idioma originalInglés
Título de la publicación alojadaRewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
EditoresKyungmin Bae
EditorialSpringer Science and Business Media Deutschland GmbH
Páginas230-250
Número de páginas21
ISBN (versión impresa)9783031124402
DOI
EstadoPublicada - 2022
Evento14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 - Munich, Alemania
Duración: 02 abr. 202203 abr. 2022

Serie de la publicación

NombreLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volumen13252 LNCS
ISSN (versión impresa)0302-9743
ISSN (versión digital)1611-3349

Conferencia

Conferencia14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
País/TerritorioAlemania
CiudadMunich
Período02/04/2203/04/22

Huella

Profundice en los temas de investigación de 'Executable Semantics and Type Checking for Session-Based Concurrency in Maude'. En conjunto forman una huella única.

Citar esto