A partial evaluation framework for order-sorted equational programs modulo axioms

DOI10.1016/j.jlamp.2019.100501zbMath1494.68048OpenAlexW2986833796WikidataQ126847592 ScholiaQ126847592MaRDI QIDQ2291823

José Meseguer, Santiago Escobar, María Alpuente, A. Cuenca-Ortega

Publication date: 31 January 2020

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

Mathematics Subject Classification ID

Applications of universal algebra in computer science (08A70) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (9)

Order-sorted equational generalization algorithm revisited ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Optimizing Maude programs via program specialization ⋮ Guest editor's foreword ⋮ Programming and symbolic computation in Maude ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Symbolic computation in Maude: some tapas

Uses Software

• Maude
• Curry
• ChC 3
• ACUOS2
• GLINTS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Strict coherence of conditional rewriting modulo axioms
• Language definitions as rewrite theories
• Complete symbolic reachability analysis using back-and-forth narrowing
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Deforestation: Transforming programs to eliminate trees
• Conditional rewriting logic as a unified model of concurrency
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Equational rules for rewriting logic
• On equational theories, unification, and (un)decidability
• Folding variant narrowing and optimal variant termination
• Programming and symbolic computation in Maude
• \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
• Partial evaluation of order-sorted equational programs modulo axioms
• A modular order-sorted equational generalization algorithm
• Order-Sorted Rewriting and Congruence Closure
• On Forward Closure and the Finite Variant Property
• Supervising Offline Partial Evaluation of Logic Programs Using Online Techniques
• A Modular Equational Generalization Algorithm
• Partial evaluation in logic programming
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• A Transformation System for Developing Recursive Programs
• The integration of functions into logic programming: From theory to practice
• Logic program specialisation through partial deduction: Control issues
• Variant-Based Satisfiability in Initial Algebras
• Functional Logic Programming: From Theory to Curry
• A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories
• Order-Sorted Generalization
• Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
• Variant Narrowing and Equational Unification
• Loop checking in partial deduction
• Term Rewriting and Applications
• Associative unification and symbolic reasoning modulo associativity in Maude

This page was built for publication: A partial evaluation framework for order-sorted equational programs modulo axioms