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

DOI10.1016/J.JLAMP.2023.100872MaRDI QIDQ6156938zbMATH OpenOpenAlexFDO

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

Publication date 19 June 2023

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1016/j.jlamp.2023.100872

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Executable Semantics and Type Checking for Session-Based Concurrency in Maude
• Session-based concurrency, declaratively
• Session types revisited
• A Semantics for Propositions as Sessions
• CONCUR 2004 - Concurrency Theory

Cites work

• scientific article; zbMATH DE number 1231536 (Why is no real title available?)
• scientific article; zbMATH DE number 1973125 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• A calculus of mobile processes. I
• A graphical approach to progress for structured communication in web services
• A new linear logic for deadlock-free session-typed processes
• A simple library implementation of binary sessions
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0
• CINNI -- a generic calculus of explicit substitutions and its application to \(\lambda\)-, \(\sigma\)- and \(\pi\)-calculi
• Characteristic bisimulation for higher-order session processes
• Deadlock and lock freedom in the linear \(\pi\)-calculus
• Executable Semantics and Type Checking for Session-Based Concurrency in Maude
• Fundamentals of session types
• Global progress for dynamically interleaved multiparty sessions
• Handbook of model checking
• Linear logic propositions as session types
• Modelling and verifying contract-oriented systems in Maude
• On the relative expressiveness of higher-order session processes
• Propositions as sessions
• Subtyping Supports Safe Session Substitution
• Subtyping for session types in the pi calculus
• The Maude LTL model checker
• Verifiable abstractions for contract-oriented systems

Cited in

(4)

• Session-based concurrency, declaratively
• Executable Semantics and Type Checking for Session-Based Concurrency in Maude
• scientific article; zbMATH DE number 2088359 (Why is no real title available?)
• Session-based concurrency, reactively

This page was built for publication: Session-based concurrency in Maude: executable semantics and type checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6156938)