Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014-11)
The notion of *operational termination* captures nonterminating computations due to subsidiary processes that are necessary to issue a *single* `main' step but which often remain `hidden' when the main computation sequence ...
Lucas Alba, Salvador; Meseguer, José(Elsevier, 2017-01)
[EN] The notion of operational termination provides a logic-based definition of termination of computational systems as the absence of infinite inferences in the computational logic describing the operational semantics of ...
Lucas Alba, Salvador; Meseguer, Jose(Elsevier, 2016-01)
We present several new concepts and results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs), which support types, subtypes and rewriting modulo axioms, and contains the ...
Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014-11)
This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems ...
Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl(Elsevier, 2018-09)
[EN] Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite ...
Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl(Springer-Verlag, 2020-10)
[EN] Proving termination of programs in `real-life¿ rewriting-based languages like CafeOBJ, Haskell, Maude, etc., is an important subject of research. To advance this goal, faithfully cap- turing the impact in the termination ...