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

DOI10.1016/j.jlamp.2023.100872zbMath1512.68173OpenAlexW4362658939MaRDI QIDQ6156938

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

Publication date: 19 June 2023

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

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

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifiable abstractions for contract-oriented systems
• Fundamentals of session types
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• A calculus of mobile processes. I
• A new linear logic for deadlock-free session-typed processes
• On the relative expressiveness of higher-order session processes
• Characteristic bisimulation for higher-order session processes
• Subtyping for session types in the pi calculus
• Propositions as sessions
• Modelling and Verifying Contract-Oriented Systems in Maude
• Subtyping Supports Safe Session Substitution
• Handbook of Model Checking
• Deadlock and lock freedom in the linear π-calculus
• A simple library implementation of binary sessions
• Global progress for dynamically interleaved multiparty sessions
• Linear logic propositions as session types

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