The rewriting logic semantics project

DOI10.1016/j.tcs.2006.12.018zbMath1111.68068OpenAlexW2139760036MaRDI QIDQ877024

Grigore Roşu, José Meseguer

Publication date: 19 April 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.018

zbMATH Keywords

rewriting logicsemantics and analysis of programming languages

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42)

Related Items

A Rewriting Logic Approach to Type Inference, José Meseguer: Scientist and Friend Extraordinaire, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, Logical approximation for program analysis, The rewriting logic semantics project: a progress report, Twenty years of rewriting logic, Rewriting semantics of production rule sets, Graph-Based Design and Analysis of Dynamic Software Architectures, Verifying hierarchical Ptolemy II discrete-event models using real-time maude, A formal library of set relations and its application to synchronous languages, From Grammars and Automata to Algebras and Coalgebras, A Maude environment for CafeOBJ, A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, An algebraic semantics for MOF, Memory Policy Analysis for Semantics Specifications in Maude, Rewriting Logic Specification of Membrane Systems with Promoters and Inhibitors, Hierarchical Design Rewriting with Maude, An overview of the K semantic framework, A compact fixpoint semantics for term rewriting systems, Abstract Certification of Global Non-interference in Rewriting Logic, Matching Logic: An Alternative to Hoare/Floyd Logic, Programming and symbolic computation in Maude, A rewriting logic approach to operational semantics, The Rewriting Logic Semantics Project: A Progress Report, A Non-Deterministic Multiset Query Language, Executable rewriting logic semantics of Orc and formal analysis of Orc programs, A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis

Uses Software

• ACL2
• JavaFAN
• LETOS
• Maude
• ITP
• 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
• Two case studies of semantics execution in Maude: CCS and LOTOS
• Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
• First-order identities as a defining language
• Conditional rewriting logic as a unified model of concurrency
• The chemical abstract machine
• Maude: specification and programming in rewriting logic
• Equational rules for rewriting logic
• Modular structural operational semantics
• A structural approach to operational semantics
• Specification and proof in membership equational logic
• A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis
• A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters
• Pragmatics of Modular SOS
• State Space Reduction of Rewrite Theories Using Invisible Transitions
• On the algebraic definition of programming languages
• Functions as processes
• Initial Algebra Semantics and Continuous Algebras
• 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
• Computer Aided Verification