Session-based concurrency in Maude: Executable semantics and type checking

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

Producción: Contribución a una revistaArtículorevisión exhaustiva


Session types are a well-established approach to communication correctness in message-passing processes. Widely studied from a process calculi perspective, here we pursue an unexplored strand and investigate the use of the Maude system for implementing session-typed process languages and reasoning about session-typed process specifications. We present four technical contributions. First, we develop and implement in Maude an executable specification of the operational semantics of a session-typed π-calculus by Vasconcelos. Second, we also develop an executable specification of its associated algorithmic type checking, and describe how both specifications can be integrated. Third, we show that our executable specification can be coupled with reachability and model checking tools in Maude to detect well-typed but deadlocked processes. Finally, we demonstrate the robustness of our approach by adapting it to a higher-order session π-calculus, in which exchanged values include names but also abstractions (functions from names to processes). All in all, our contributions define a promising new approach to the (semi)automated analysis of communication correctness in message-passing concurrency.

Idioma originalInglés
Número de artículo100872
PublicaciónJournal of Logical and Algebraic Methods in Programming
EstadoPublicada - jun. 2023


Profundice en los temas de investigación de 'Session-based concurrency in Maude: Executable semantics and type checking'. En conjunto forman una huella única.

Citar esto