Optimization of rewrite theories by equational partial evaluation

DOI10.1016/J.JLAMP.2021.100729MaRDI QIDQ2667190zbMATH OpenOpenAlexFDO

Authors María Alpuente, Santiago Escobar, Julia Sapiña, D. Ballis

Publication date 24 November 2021

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

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Grammars and rewriting systems (68Q42) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A partial evaluation framework for order-sorted equational programs modulo axioms
• Partial evaluation of order-sorted equational programs modulo axioms
• scientific article; zbMATH DE number 2038715
• Equational abstractions for reducing the state space of rewrite theories
• Semantic foundations for generalized rewrite theories

Cites work

• \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
• A Modular Equational Generalization Algorithm
• A modular order-sorted equational generalization algorithm
• A partial evaluation framework for order-sorted equational programs modulo axioms
• A Transformation System for Developing Recursive Programs
• Abstract logical model checking of infinite-state systems using narrowing
• ACUOS: a system for modular ACU generalization with subtyping and inheritance
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Associative unification and symbolic reasoning modulo associativity in Maude
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Conditional rewriting logic as a unified model of concurrency
• Conjunctive partial deduction: foundations, control, algorithms, and experiments
• Equational abstractions
• Equational rules for rewriting logic
• Folding variant narrowing and optimal variant termination
• Generalized rewrite theories, coherence completion, and symbolic methods
• scientific article; zbMATH DE number 1222408 (Why is no real title available?)
• scientific article; zbMATH DE number 1088019 (Why is no real title available?)
• scientific article; zbMATH DE number 1950450 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Metalevel algorithms for variant satisfiability
• MTT: The Maude Termination Tool (System Description)
• On Forward Closure and the Finite Variant Property
• Order-sorted generalization
• Partial evaluation in logic programming
• Specialization of functional logic programs based on needed narrowing
• Strict coherence of conditional rewriting modulo axioms
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Term Rewriting and Applications
• Variant narrowing and equational unification
• Variant-Based Satisfiability in Initial Algebras

Cited in

(4)

• Partial evaluation of order-sorted equational programs modulo axioms
• On the Expressivity of Optimality Theory versus Ordered Rewrite Rules
• Symbolic Specialization of Rewriting Logic Theories with Presto
• Optimizing Maude programs via program specialization

Describes a project that uses

Uses Software

• GLINTS
• Maude
• Maude-NPA
• ACUOS2
• ECCE
• MTT

This page was built for publication: Optimization of rewrite theories by equational partial evaluation

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