MTT: The Maude termination tool. Despite the remarkable development of the theory of termination of rewriting, its application to high-level programming languages is far from being optimal. This is due to the need for features such as conditional equations and rules, types and subtypes, (possibly programmable) strategies for controlling the execution, matching modulo axioms, and so on, that are used in many programs and tend to place such programs outside the scope of current termination tools. The operational meaning of such features is often formalized in a proof-theoretic manner by means of an inference system rather than just by a rewriting relation. In particular, Generalized Rewrite Theories (GRT) are a recent generalization of rewrite theories at the heart of the most recent formulation of Maude.

References in zbMATH (referenced in 25 articles )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Alpuente, M.; Ballis, D.; Escobar, S.; Sapiña, J.: Optimization of rewrite theories by equational partial evaluation (2022)
  2. Lucas, Salvador: Applications and extensions of context-sensitive rewriting (2021)
  3. Meseguer, José: Symbolic computation in Maude: some tapas (2021)
  4. Durán, Francisco; Meseguer, José; Rocha, Camilo: Ground confluence of order-sorted conditional specifications modulo axioms (2020)
  5. Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques (2020)
  6. Aguirre, Luis; Martí-Oliet, Narciso; Palomino, Miguel; Pita, Isabel: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude (2018)
  7. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  8. Clavel, Manuel; Durán, Francisco; Eker, Steven; Escobar, Santiago; Lincoln, Patrick; Martí-Oliet, Narciso; Talcott, Carolyn: Two decades of Maude (2015)
  9. Lucas, Salvador; Meseguer, José: Localized operational termination in general logics (2015)
  10. Roşu, Grigore; Lucanu, Dorel: Behavioral rewrite systems and behavioral productivity (2014)
  11. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  12. Durán, Francisco; Meseguer, José: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories (2012)
  13. Meseguer, José: Twenty years of rewriting logic (2012)
  14. Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador; Navarro-Marset, Rafael: Proving termination properties with \textscmu-term (2011)
  15. Alpuente, María; Escobar, Santiago; Iborra, José: Modular termination of basic narrowing and equational unification (2011)
  16. Codescu, Mihai; Mossakowski, Till; Riesco, Adrián; Maeder, Christian: Integrating Maude into Hets (2011)
  17. Alpuente, M.; Comini, M.; Escobar, S.; Falaschi, M.; Iborra, J.: A compact fixpoint semantics for term rewriting systems (2010)
  18. Durán, Francisco; Meseguer, José: A Maude coherence checker tool for conditional order-sorted rewrite theories (2010)
  19. Durán, Francisco; Meseguer, José: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications (2010)
  20. Durán, Francisco; Lucas, Salvador; Meseguer, José: Methods for proving termination of rewriting-based programming languages by transformation (2009)

1 2 next