Language definitions as rewrite theories

DOI10.1016/J.JLAMP.2015.09.001MaRDI QIDQ730476zbMATH OpenOpenAlexFDO

Authors Vlad Rusu, Dorel Lucanu, Traian Şerbănuţă, Andrei Arusoaie, A. Stefanescu, Grigore Roşu

Publication date 28 December 2016

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.2015.09.001

zbMATH Keywords

operational semanticssymbolic executionMaudeK frameworkrewrite theories

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

Recommendations

• Language definitions as rewrite theories
• K-Maude: a rewriting based tool for semantics of programming languages
• A rewrite framework for language definitions and for generation of efficient interpreters
• Symbolic execution based on language transformation
• Executable structural operational semantics in Maude

Cites work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An overview of the K semantic framework
• Equational abstractions
• Equational rules for rewriting logic
• K-Maude: a rewriting based tool for semantics of programming languages
• Language definitions as rewrite theories
• Matching logic -- extended abstract (invited talk)
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• One-path reachability logic
• Rewriting modulo SMT and open system analysis
• State Space Reduction of Rewrite Theories Using Invisible Transitions

Cited in

(7)

• A partial evaluation framework for order-sorted equational programs modulo axioms
• Symbolic execution based on language transformation
• Language definitions as rewrite theories
• A generic framework for symbolic execution: a coinductive approach
• Executing and verifying higher-order functional-imperative programs in Maude
• K-Maude: a rewriting based tool for semantics of programming languages
• A Maude environment for CafeOBJ

Describes a project that uses

Uses Software

• K Prover
• K-Maude
• K tool
• Maude
• z3

This page was built for publication: Language definitions as rewrite theories

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