[EN] Partial evaluation is a powerful and general program optimization technique with many successful applications. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ...
[EN] The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been ...
Durán, Francisco; Eker, Steven; Escobar Román, Santiago; NARCISO MARTÍ OLIET; José Meseguer; Rubén Rubio; Talcott, Carolyn(Elsevier, 2020-01)
[EN] Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs ...
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 ...
[EN] Decision procedures can be either theory-specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for ...