A rewriting logic approach to operational semantics

DOI10.1016/j.ic.2008.03.026zbMath1165.68041OpenAlexW1983696848MaRDI QIDQ1012130

Grigore Roşu, José Meseguer, Traian-Florin Şerbănuţă

Publication date: 14 April 2009

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2008.03.026

zbMATH Keywords

operational semanticsrewriting logicrewriting logic semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42)

Related Items (15)

Equational logic and categorical semantics for multi-languages ⋮ Converting between Combinatory Reduction Systems and Big Step Semantics ⋮ From Rewriting Logic, to Programming Language Semantics, to Program Verification ⋮ The rewriting logic semantics project: a progress report ⋮ Twenty years of rewriting logic ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ A language-independent proof system for full program equivalence ⋮ Symbolic execution based on language transformation ⋮ An algebraic semantics for MOF ⋮ An overview of the K semantic framework ⋮ Programming and symbolic computation in Maude ⋮ Finding a Forest in a Tree ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ Executable rewriting logic semantics of Orc and formal analysis of Orc programs ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract)

Uses Software

• ACL2
• ML
• Stratego
• JavaFAN
• ELAN
• OBJ3
• CafeOBJ
• Maude
• MMT
• PMaude
• Centaur
• K Prover
• Java+ITP

Cites Work

• 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
• The gamma model and its discipline of programming
• The rewriting logic semantics project
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• First-order identities as a defining language
• Conditional rewriting logic as a unified model of concurrency
• The chemical abstract machine
• A syntactic approach to type soundness
• ELAN from a rewriting logic point of view
• Maude: specification and programming in rewriting logic
• Equational rules for rewriting logic
• Rewriting logic: Roadmap and bibliography
• Modular structural operational semantics
• A structural approach to operational semantics
• Executable structural operational semantics in Maude
• Semantic foundations for generalized rewrite theories
• Language Prototyping: An Algebraic Specification Approach
• Deduction, Strategies, and Rewriting
• A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis
• Partial Order Reduction for Rewriting Semantics of Programming Languages
• A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters
• Pragmatics of Modular SOS
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Representing and Reasoning with Operational Semantics
• On the algebraic definition of programming languages
• Functions as processes
• A framework for defining logics
• Evolving Algebras 1993: Lipari Guide
• Explicit substitutions
• Unified Algebras and action semantics
• Automated Reasoning
• Computer Aided Verification
• Algebraic Methodology and Software Technology
• Algebraic Methodology and Software Technology
• Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
• Theoretical Aspects of Computing – ICTAC 2005
• Computer Aided Verification
• Rewriting logic as a semantic framework for concurrency: a progress report

This page was built for publication: A rewriting logic approach to operational semantics