An Incremental Needed Narrowing Calculus for Curry. - María Alpuente; Salvador Lucas; Santiago Escobar 001 (APPIA-GULP-PRODE, 1999)

UPV-CURRY: An Incremental CURRY Interpreter. - María Alpuente; Santiago Escobar 001; Salvador Lucas (SOFSEM, 1999)

Redundancy Analyses in Term Rewriting. - María Alpuente; Santiago Escobar 001; Salvador Lucas (WFLP, 2000)

Removing Redundant Arguments of Functions. - María Alpuente; Santiago Escobar 001; Salvador Lucas (AMAST, 2002)

Abstract Diagnosis of Functional Programs. - María Alpuente; Marco Comini; Santiago Escobar 001; Moreno Falaschi; Salvador Lucas (LOPSTR, 2002)

Improving On-Demand Strategy Annotations. - María Alpuente; Santiago Escobar 001; Bernhard Gramlich; Salvador Lucas (LPAR, 2002)

Redundancy of Arguments Reduced to Induction. - María Alpuente; Rachid Echahed; Santiago Escobar 001; Salvador Lucas (WFLP, 2002)

Correct and Complete (Positive) Strategy Annotations for OBJ. - María Alpuente; Santiago Escobar 001; Salvador Lucas (WRLA, 2002)

Abstract Correction of OBJ-like Programs. - María Alpuente; Demis Ballis; Santiago Escobar 001; Moreno Falaschi; Salvador Lucas (APPIA-GULP-PRODE, 2003)

Refining weakly outermost-needed rewriting and narrowing. - Santiago Escobar 001 (PPDP, 2003)

Abstract correction of first-order functional programs. - María Alpuente; Demis Ballis; Santiago Escobar 001; Moreno Falaschi; Salvador Lucas (WFLP, 2003)

OnDemandOBJ: A Laboratory for Strategy Annotations. - María Alpuente; Santiago Escobar 001; Salvador Lucas (RULE@RDP, 2003)

On-demand Evaluation by Program Transformation. - María Alpuente; Santiago Escobar 001; Salvador Lucas (RULE@RDP, 2003)

Implementing Natural Rewriting and Narrowing Efficiently. - Santiago Escobar 001 (FLOPS, 2004)

Natural Rewriting for General Term Rewriting Systems. - Santiago Escobar 001; José Meseguer 001; Prasanna Thati (LOPSTR, 2004)

Thesis: Strategies and analysis techniques in functional program optimization. - Santiago Escobar 001 (AI Commun., 2004)

New Evaluation Commands for Maude Within Full Maude. - Francisco Durán 001; Santiago Escobar 001; Salvador Lucas (WRLA, 2004)

On-demand Evaluation for Maude. - Francisco Durán 001; Santiago Escobar 001; Salvador Lucas (RULE@RDP, 2004)

A rewriting-based inference system for the NRL protocol analyzer: grammar generation. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (FMSE, 2005)

Natural Narrowing for General Term Rewriting Systems. - Santiago Escobar 001; José Meseguer 001; Prasanna Thati (RTA, 2005)

Preface. - María Alpuente; Santiago Escobar 001; Moreno Falaschi (WWV, 2005)

Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (SecReT@ICALP, 2006)

Narrowing and Rewriting Logic: from Foundations to Applications. - Santiago Escobar 001; José Meseguer 001; Prasanna Thati (WFLP, 2006)

A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (Theor. Comput. Sci., 2006)

Automatic Certification of Java Source Code in Rewriting Logic. - Mauricio Alba-Castro; María Alpuente; Santiago Escobar 001 (FMICS, 2007)

Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (FOSAD, 2007)

Symbolic Model Checking of Infinite-State Systems Using Narrowing. - Santiago Escobar 001; José Meseguer 001 (RTA, 2007)

Preface. - Demis Ballis; Santiago Escobar 001; Massimo Marchiori (WWV, 2007)

Removing redundant arguments automatically. - María Alpuente; Santiago Escobar 001; Salvador Lucas (Theory Pract. Log. Program., 2007)

State Space Reduction in the Maude-NRL Protocol Analyzer. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (ESORICS, 2008)

Automated Certification of Non-Interference in Rewriting Logic. - Mauricio Alba-Castro; María Alpuente; Santiago Escobar 001 (FMICS, 2008)

Termination of Narrowing Using Dependency Pairs. - María Alpuente; Santiago Escobar 001; José Iborra (ICLP, 2008)

A Modular Equational Generalization Algorithm. - María Alpuente; Santiago Escobar 001; José Meseguer 001; Pedro Ojeda (LOPSTR, 2008)

Directed-Logical Testing for Functional Verification of Microprocessors. - Michael Katelman; José Meseguer 001; Santiago Escobar 001 (MEMOCODE, 2008)

Modular Termination of Basic Narrowing. - María Alpuente; Santiago Escobar 001; José Iborra (RTA, 2008)

Effectively Checking the Finite Variant Property. - Santiago Escobar 001; José Meseguer 001; Ralf Sasse (RTA, 2008)

Equational Unification by Variant Narrowing (Extended Abstract). - Santiago Escobar 001; José Meseguer 001; Ralf Sasse (UNIF, 2008)

A Tool for Automated Certification of Java Source Code in Maude. - Mauricio Alba-Castro; María Alpuente; Santiago Escobar 001; Pedro Ojeda; Daniel Romero 001 (PROLE, 2008)

Order-Sorted Generalization. - María Alpuente; Santiago Escobar 001; José Meseguer 001; Pedro Ojeda (WFLP, 2008)

Preface. - Demis Ballis; Santiago Escobar 001 (WWV, 2008)

Preface. - Daniel J. Dougherty; Santiago Escobar 001 (SecReT@LICS/CSF, 2008)

Variant Narrowing and Equational Unification. - Santiago Escobar 001; José Meseguer 001; Ralf Sasse (WRLA, 2008)

Abstract Certification of Global Non-interference in Rewriting Logic. - Mauricio Alba-Castro; María Alpuente; Santiago Escobar 001 (FMCO, 2009)

Unification and Narrowing in Maude 2.4. - Manuel Clavel; Francisco Durán 001; Steven Eker; Santiago Escobar 001; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (RTA, 2009)

A Graphical User Interface for Maude-NPA. - Sonia Santiago; Carolyn L. Talcott; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (PROLE, 2009)

Termination of narrowing revisited. - María Alpuente; Santiago Escobar 001; José Iborra (Theor. Comput. Sci., 2009)

Sequential Protocol Composition in Maude-NPA. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (ESORICS, 2010)

Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA. - Ralf Sasse; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (STM, 2010)

Approximating Non-interference and Erasure in Rewriting Logic. - Mauricio Alba-Castro; María Alpuente; Santiago Escobar 001 (SYNASC, 2010)

A compact fixpoint semantics for term rewriting systems. - María Alpuente; Marco Comini; Santiago Escobar 001; Moreno Falaschi; José Iborra (Theor. Comput. Sci., 2010)

On-demand strategy annotations revisited: An improved on-demand evaluation strategy. - María Alpuente; Santiago Escobar 001; Bernhard Gramlich; Salvador Lucas (Theor. Comput. Sci., 2010)

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. - Santiago Escobar 001; Deepak Kapur; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Ralf Sasse (PPDP, 2011)

Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; José Meseguer 001; Carolyn L. Talcott (RTA, 2011)

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Ralf Sasse (UNIF, 2011)

Modular termination of basic narrowing and equational unification. - María Alpuente; Santiago Escobar 001; José Iborra (Log. J. IGPL, 2011)

The use of types in designing unification algorithms: two case studies. - Serdar Erbatur; Santiago Escobar 001; Paliath Narendran (UNIF, 2012)

Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Sonia Santiago; Ralf Sasse (ESORICS, 2012)

Folding variant narrowing and optimal variant termination. - Santiago Escobar 001; Ralf Sasse; José Meseguer 001 (J. Log. Algebraic Methods Program., 2012)

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Sonia Santiago; Ralf Sasse (CADE, 2013)

Incremental and Adaptive Software Systems Development of Natural Language Applications. - Elena Lloret; Santiago Escobar 001; Manuel Palomar; Isidro Ramos (ISD, 2013)

Detecting Modular ACU Structural Symmetries. - María Alpuente; Santiago Escobar 001; Javier Espert (UNIF@RTA/TLCA, 2013)

Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. - Kyungmin Bae; Santiago Escobar 001; José Meseguer 001 (RTA, 2013)

Unification and Anti-unification modulo Equational Theories. - Santiago Escobar 001 (UNIF@RTA/TLCA, 2013)

Functional Logic Programming in Maude. - Santiago Escobar 001 (Specification, Algebra, and Software, 2014)

A rewriting-based forwards semantics for Maude-NPA. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (HotSoS, 2014)

ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance. - María Alpuente; Santiago Escobar 001; Javier Espert; José Meseguer 001 (JELIA, 2014)

Theories of Homomorphic Encryption, Unification, and the Finite Variant Property. - Fan Yang 090; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Paliath Narendran (PPDP, 2014)

Analysis of the IBM CCA Security API Protocols in Maude-NPA. - Antonio González-Burgueño; Sonia Santiago; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (SSR, 2014)

A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA. - Sonia Santiago; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (STM, 2014)

A modular order-sorted equational generalization algorithm. - María Alpuente; Santiago Escobar 001; Javier Espert; José Meseguer 001 (Inf. Comput., 2014)

Functional and (Constraint) Logic Programming. - Santiago Escobar 001; Moreno Falaschi (Inf. Comput., 2014)

State space reduction in the Maude-NRL Protocol Analyzer. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (Inf. Comput., 2014)

Two Decades of Maude. - Manuel Clavel; Francisco Durán 001; Steven Eker; Santiago Escobar 001; Patrick Lincoln; Narciso Martí-Oliet; Carolyn L. Talcott (Logic, Rewriting, and Concurrency, 2015)

Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (Programming Languages with Applications to Biology and Security, 2015)

Analysis of the PKCS#11 API Using the Maude-NPA Tool. - Antonio González-Burgueño; Sonia Santiago; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (SSR, 2015)

Constrained narrowing for conditional equational theories modulo axioms. - Andrew Cholewa; Santiago Escobar 001; José Meseguer 001 (Sci. Comput. Program., 2015)

Built-in Variant Generation and Unification, and Their Applications in Maude 2.7. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (IJCAR, 2016)

Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms. - María Alpuente; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (LOPSTR, 2016)

Strand spaces with choice via a process algebra semantics. - Fan Yang 090; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (PPDP, 2016)

Effective Sequential Protocol Composition in Maude-NPA. - Sonia Santiago; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (CoRR, 2016)

Rewriting logic and its applications (extended selected papers from WRLA 2014). - Santiago Escobar 001 (J. Log. Algebraic Methods Program., 2016)

Inspecting Maude variants with GLINTS. - María Alpuente; Santiago Escobar 001; Julia Sapiña; Angel Cuenca-Ortega (Theory Pract. Log. Program., 2017)

Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms. - María Alpuente; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (LOPSTR, 2018)

Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA. - Antonio González-Burgueño; Damián Aparicio-Sánchez; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (LPAR, 2018)

Modular Verification of Sequential Composition for Private Channels in Maude-NPA. - Fan Yang 090; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (STM, 2018)

Associative Unification and Symbolic Reasoning Modulo Associativity in Maude. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (WRLA@ETAPS, 2018)

Multi-paradigm Programming in Maude. - Santiago Escobar 001 (WRLA@ETAPS, 2018)

Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method. - Santiago Escobar 001; José Meseguer 001 (Foundations of Security, Protocols, and Equational Reasoning, 2019)

ACUOS2: A High-Performance System for Modular ACU Generalization with Subtyping and Inheritance. - María Alpuente; Demis Ballis; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (JELIA, 2019)

Strand Spaces with Choice via a Process Algebra Semantics. - Fan Yang 090; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (CoRR, 2019)

Most General Variant Unifiers. - Santiago Escobar 001; Julia Sapiña (ICLP Technical Communications, 2019)

Symbolic Analysis of Maude Theories with Narval. - María Alpuente; Santiago Escobar 001; Julia Sapiña; Demis Ballis (Theory Pract. Log. Program., 2019)

An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA. - Damián Aparicio-Sánchez; Santiago Escobar 001; Raúl Gutiérrez; Julia Sapiña (ESORICS (2), 2020)

Protocol Analysis with Time. - Damián Aparicio-Sánchez; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Julia Sapiña (INDOCRYPT, 2020)

Variant-based Equational Unification under Constructor Symbols. - Damián Aparicio-Sánchez; Santiago Escobar 001; Julia Sapiña (ICLP Technical Communications, 2020)

Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms. - María Alpuente; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (Fundam. Informaticae, 2020)

A partial evaluation framework for order-sorted equational programs modulo axioms. - María Alpuente; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (J. Log. Algebraic Methods Program., 2020)

Programming and symbolic computation in Maude. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Rubén Rubio; Carolyn L. Talcott (J. Log. Algebraic Methods Program., 2020)

Protocol Analysis with Time and Space. - Damián Aparicio-Sánchez; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Julia Sapiña (Protocols, Strands, and Logic, 2021)

Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description). - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Rubén Rubio; Carolyn L. Talcott (IJCAR, 2022)

Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude. - Víctor García; Santiago Escobar 001; Kazuhiro Ogata 001 (FAVPQC@ICFEM, 2022)

Canonical Narrowing for Variant-Based Conditional Rewrite Theories. - Raúl López-Rueda; Santiago Escobar 001 (ICFEM, 2022)

Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (FAVPQC@ICFEM, 2022)

Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis. - Duong Dinh Tran; Canh Minh Do; Santiago Escobar 001; Kazuhiro Ogata 001 (FAVPQC@ICFEM, 2022)

Variant-Based Equational Anti-unification. - María Alpuente; Demis Ballis; Santiago Escobar 001; Julia Sapiña (LOPSTR, 2022)

Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (SEKE, 2022)

Parallel Maude-NPA for Cryptographic Protocol Analysis. - Canh Minh Do; Adrián Riesco 001; Santiago Escobar 001; Kazuhiro Ogata 001 (WRLA@ETAPS, 2022)

Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method. - Raúl López-Rueda; Santiago Escobar 001 (WRLA@ETAPS, 2022)

An Efficient Canonical Narrowing Implementation for Protocol Analysis. - Raúl López-Rueda; Santiago Escobar 001; José Meseguer 001 (WRLA@ETAPS, 2022)

Order-sorted equational generalization algorithm revisited. - María Alpuente; Santiago Escobar 001; José Meseguer 001; Julia Sapiña (Ann. Math. Artif. Intell., 2022)

Optimization of rewrite theories by equational partial evaluation. - María Alpuente; Demis Ballis; Santiago Escobar 001; Julia Sapiña (J. Log. Algebraic Methods Program., 2022)

Symbolic Specialization of Rewriting Logic Theories with Presto. - María Alpuente; Santiago Escobar 001; Julia Sapiña; Demis Ballis (Theory Pract. Log. Program., 2022)

Optimizing Maude Programs via Program Specialization. - María Alpuente; Demis Ballis; Santiago Escobar 001; José Meseguer 001; Julia Sapiña (Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems, 2023)

Protocol Dialects as Formal Patterns. - D. Galán; Víctor García; Santiago Escobar 001; Catherine A. Meadows; José Meseguer 001 (ESORICS (2), 2023)

Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints. - Santiago Escobar 001; Raúl López-Rueda; Julia Sapiña (FTSCS, 2023)

Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (IET Inf. Secur., 2023)

Modelling and verification of post-quantum key encapsulation mechanisms using Maude. - Víctor García; Santiago Escobar 001; Kazuhiro Ogata 001; Sedat Akleylek; Ayoub Otmani (PeerJ Comput. Sci., 2023)

Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version. - Duong Dinh Tran; Canh Minh Do; Santiago Escobar 001; Kazuhiro Ogata 001 (PeerJ Comput. Sci., 2023)

Safety enforcement via programmable strategies in Maude. - María Alpuente; Demis Ballis; Santiago Escobar 001; D. Galán; Julia Sapiña (J. Log. Algebraic Methods Program., 2023)

An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis. - Raúl López-Rueda; Santiago Escobar 001; Julia Sapiña (J. Log. Algebraic Methods Program., 2023)

NuITP: An Inductive Theorem Prover for Equational Program Verification. - Francisco J. Durán; Santiago Escobar 001; José Meseguer 001; Julia Sapiña (PPDP, 2024)

Programming Open Distributed Systems in Maude. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Rubén Rubio; Carolyn L. Talcott (PPDP, 2024)

Verifying Invariants by Deductive Model Checking. - Kyungmin Bae; Santiago Escobar 001; Raúl López-Rueda; José Meseguer 001; Julia Sapiña (WRLA, 2024)

Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (IEEE Access, 2024)

Preface to Rewriting Logic and Its Applications (revised selected papers from WRLA 2020). - Santiago Escobar 001; Narciso Martí-Oliet (J. Log. Algebraic Methods Program., 2025)

Formalization and analysis of the post-quantum signature scheme FALCON with Maude. - Víctor García; Santiago Escobar 001; Kazuhiro Ogata 001 (J. Log. Algebraic Methods Program., 2025)

Protocol Dialects as Formal Patterns: A Composable Theory of Lingos - Technical report. - Víctor García; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (CoRR, 2025)