Executable structural operational semantics in Maude

DOI10.1016/j.jlap.2005.09.008zbMath1088.68095OpenAlexW1981466053WikidataQ123905888 ScholiaQ123905888MaRDI QIDQ2369036

Narciso Martí-Oliet, Alberto Verdejo

Publication date: 28 April 2006

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: http://eprints.ucm.es/4888/1/08-TR-134-03-esim.pdf

zbMATH Keywords

Rewriting logicCCSLOTOSACT ONEStructural operational semanticsExecutabilityMaude 2Metalanguage

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (12)

From Rewriting Logic, to Programming Language Semantics, to Program Verification ⋮ The rewriting logic semantics project: a progress report ⋮ Twenty years of rewriting logic ⋮ A Maude environment for CafeOBJ ⋮ Hierarchical Design Rewriting with Maude ⋮ Semantic foundations for generalized rewrite theories ⋮ A process calculus BigrTiMo of mobile systems and its formal semantics ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ A rewriting logic approach to operational semantics ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ Modular Structural Operational Semantics with Strategies ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract)

Uses Software

• Coq
• ML
• LOTOS
• Maude
• Eden

Cites Work

• Symbolic bisimulations
• Conditional rewriting logic as a unified model of concurrency
• Winskel is (almost) right: Towards a mechanized semantics textbook
• IThe 2nd international workshop on rewriting logic and its applications, RWLW.. Abbaye des Prèmontrès at Pont-á-Mousson, France, September 1998
• \(\pi\)-calculus in (Co)inductive-type theory
• Isabelle/HOL. A proof assistant for higher-order logic
• A causal semantics for CCS via rewriting logic
• Maude: specification and programming in rewriting logic
• Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
• Rewriting logic: Roadmap and bibliography
• Handbook of philosophical logic. Vol. 9
• Specification and proof in membership equational logic
• Algebraic laws for nondeterminism and concurrency
• Theories of Programming Languages
• A Modal Logic for Full LOTOS based on Symbolic Transition Systems
• Encoding natural semantics in Coq
• Algebraic Methodology and Software Technology
• Generic tools for verifying concurrent systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Executable structural operational semantics in Maude