El lambda-calculo Etiquetado Paralelo (LCEP). - Salvador Lucas; Javier Oliver 001 (GULP-PRODE (1), 1994)

Computational Properties in Context-Sensitive Rewriting. - Salvador Lucas (GULP-PRODE, 1995)

Fundamentals of Context=Sensitive Rewriting. - Salvador Lucas (SOFSEM, 1995)

A Denotational Semantics for Needed Narrowing. - Michael Hanus; Salvador Lucas (APPIA-GULP-PRODE, 1996)

Termination of Context-Sensitive Rewriting by Rewriting. - Salvador Lucas (ICALP, 1996)

Context-Sensitive Computations in Confluent Programs. - Salvador Lucas (PLILP, 1996)

A New Proposal of Concurrent Process Calculus. - Salvador Lucas; Javier Oliver 001 (SOFSEM, 1996)

Computational Properties of Term Rewriting with Replacement Restrictions. - Salvador Lucas (APPIA-GULP-PRODE, 1997)

Needed Reductions with Context-Sensitive Rewriting. - Salvador Lucas (ALP/HOA, 1997)

Transformations for Efficient Evaluations in Functional Programming. - Salvador Lucas (PLILP, 1997)

Efficient Strong Sequentiality Using Replacement Restrictions. - Salvador Lucas (SOFSEM, 1997)

Strongly Sequential and Inductively Sequential Term Rewriting Systems. - Michael Hanus; Salvador Lucas; Aart Middeldorp (Inf. Process. Lett., 1998)

Root-Neededness and Approximations of Neededness. - Salvador Lucas (Inf. Process. Lett., 1998)

Context-sensitive Computations in Functional and Functional Logic Programs. - Salvador Lucas (J. Funct. Log. Program., 1998)

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

A Semantics for Program Analysis in Narrowing-Based Functional Logic Languages. - Michael Hanus; Salvador Lucas (Fuji International Symposium on Functional and Logic Programming, 1999)

Specialization of Inductively Sequential Functional Logic Programs. - María Alpuente; Michael Hanus; Salvador Lucas; Germán Vidal (ICFP, 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)

Redundant arguments in infinitary rewriting. - Salvador Lucas (WFLP, 2000)

Termination of Rewriting With Strategy Annotations. - Salvador Lucas (LPAR, 2001)

Termination of On-Demand Rewriting and Termination of OBJ Programs. - Salvador Lucas (PPDP, 2001)

Transfinite Rewriting Semantics for Term Rewriting Systems. - Salvador Lucas (RTA, 2001)

Lazy Rewriting and Context-Sensitive Rewriting. - Salvador Lucas (WFLP, 2001)

An Evaluation Semantics for Narrowing-Based Functional Logic Languages. - Michael Hanus; Salvador Lucas (J. Funct. Log. Program., 2001)

1st International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2001) - Preface. - Bernhard Gramlich; Salvador Lucas (WRS, 2001)

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

Recursive Path Orderings Can Be Context-Sensitive. - Cristina Borralleras; Salvador Lucas; Albert Rubio (CADE, 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)

Modular termination of context-sensitive rewriting. - Bernhard Gramlich; Salvador Lucas (PPDP, 2002)

Termination of (Canonical) Context-Sensitive Rewriting. - Salvador Lucas (RTA, 2002)

Simple termination of context-sensitive rewriting. - Bernhard Gramlich; Salvador Lucas (ACM SIGPLAN Workshop on Rule-Based Programming, 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)

Demandness in Rewriting and Narrowing. - Sergio Antoy; Salvador Lucas (WFLP, 2002)

Preface. - Bernhard Gramlich; Salvador Lucas (WRS, 2002)

Context-Sensitive Rewriting Strategies. - Salvador Lucas (Inf. Comput., 2002)

Abstract Correction of OBJ-like Programs. - María Alpuente; Demis Ballis; Santiago Escobar 001; Moreno Falaschi; Salvador Lucas (APPIA-GULP-PRODE, 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)

Preface: 3rd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2003) - Final Proceedings. - Bernhard Gramlich; Salvador Lucas (WRS, 2003)

Polynomials for Proving Termination of Context-Sensitive Rewriting. - Salvador Lucas (FoSSaCS, 2004)

Proving termination of membership equational programs. - Francisco Durán 001; Salvador Lucas; José Meseguer 001; Claude Marché; Xavier Urbain (PEPM, 2004)

mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting. - Salvador Lucas (RTA, 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)

Strategies in Programming Languages Today. - Salvador Lucas (WRS, 2004)

Preface. - Salvador Lucas (PROLE, 2004)

Strong and NV-sequentiality of constructor systems. - Salvador Lucas (Inf. Process. Lett., 2004)

Termination of Fair Computations in Term Rewriting. - Salvador Lucas; José Meseguer 001 (LPAR, 2005)

Rewriting-based navigation of Web sites. - Salvador Lucas (WWV, 2005)

Rewriting-Based Navigation of Web Sites: Looking for Models and Logics. - Salvador Lucas (WWV, 2005)

Operational termination of conditional term rewriting systems. - Salvador Lucas; Claude Marché; José Meseguer 001 (Inf. Process. Lett., 2005)

Polynomials over the reals in proofs of termination: from theory to practice. - Salvador Lucas (RAIRO Theor. Informatics Appl., 2005)

Reduction strategies in rewriting and programming. - Bernhard Gramlich; Salvador Lucas (J. Symb. Comput., 2005)

Specialization of functional logic programs based on needed narrowing. - María Alpuente; Salvador Lucas; Michael Hanus; Germán Vidal (Theory Pract. Log. Program., 2005)

Generalizing Newman's Lemma for Left-Linear Rewrite Systems. - Bernhard Gramlich; Salvador Lucas (RTA, 2006)

On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. - Salvador Lucas (Appl. Algebra Eng. Commun. Comput., 2006)

Proving Termination of Context-Sensitive Rewriting with MU-TERM. - Beatriz Alarcón; Raúl Gutiérrez; José Iborra; Salvador Lucas (PROLE, 2006)

Improving the Context-sensitive Dependency Graph. - Beatriz Alarcón; Raúl Gutiérrez; Salvador Lucas (PROLE, 2006)

Proving termination of context-sensitive rewriting by transformation. - Salvador Lucas (Inf. Comput., 2006)

The Maude Formal Tool Environment. - Manuel Clavel; Francisco Durán 001; Joe Hendrix; Salvador Lucas; José Meseguer 001; Peter Csaba Ölveczky (CALCO, 2007)

Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs. - Beatriz Alarcón; Salvador Lucas (FroCoS, 2007)

Practical use of polynomials over the reals in proofs of termination. - Salvador Lucas (PPDP, 2007)

Formal Verification of Websites. - Sonia Flores; Salvador Lucas; Alicia Villanueva (WWV, 2007)

Comparing CSP and SAT Solvers for Polynomial Constraints in Termination Provers. - Salvador Lucas; Rafael Navarro-Marset (PROLE, 2007)

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

Search Techniques for Rational Polynomial Orders. - Carsten Fuhs; Rafael Navarro-Marset; Carsten Otto; Jürgen Giesl; Salvador Lucas; Peter Schneider-Kamp (AISC/MKM/Calculemus, 2008)

MTT: The Maude Termination Tool (System Description). - Francisco Durán 001; Salvador Lucas; José Meseguer 001 (IJCAR, 2008)

Improving Context-Sensitive Dependency Pairs. - Beatriz Alarcón; Fabian Emmes; Carsten Fuhs; Jürgen Giesl; Raúl Gutiérrez; Salvador Lucas; Peter Schneider-Kamp; René Thiemann (LPAR, 2008)

Order-sorted dependency pairs. - Salvador Lucas; José Meseguer 001 (PPDP, 2008)

Usable Rules for Context-Sensitive Rewrite Systems. - Raúl Gutiérrez; Salvador Lucas; Xavier Urbain (RTA, 2008)

Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting. - Beatriz Alarcón; Salvador Lucas (PROLE, 2008)

Methods for Proving Termination of Rewriting-based Programming Languages by Transformation. - Francisco Durán 001; Salvador Lucas; José Meseguer 001 (PROLE, 2008)

Web Services and Interoperability for the Maude Termination Tool. - Francisco Durán 001; Salvador Lucas; José Meseguer 001; Francisco Gutiérrez (PROLE, 2008)

Operational Termination of Membership Equational Programs: the Order-Sorted Way. - Salvador Lucas; José Meseguer 001 (WRLA, 2008)

Termination of just/fair computations in term rewriting. - Salvador Lucas; José Meseguer 001 (Inf. Comput., 2008)

Proving operational termination of membership equational programs. - Francisco Durán 001; Salvador Lucas; Claude Marché; José Meseguer 001; Xavier Urbain (High. Order Symb. Comput., 2008)

Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. - Cristina Borralleras; Salvador Lucas; Rafael Navarro-Marset; Enric Rodríguez-Carbonell; Albert Rubio (CADE, 2009)

Termination Modulo Combinations of Equational Theories. - Francisco Durán 001; Salvador Lucas; José Meseguer 001 (FroCoS, 2009)

Automatic Proofs of Termination With Elementary Interpretations. - Salvador Lucas (PROLE, 2009)

From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals. - Salvador Lucas (AISC/MKM/Calculemus, 2010)

Proving Termination Properties with mu-term. - Beatriz Alarcón; Raúl Gutiérrez; Salvador Lucas; Rafael Navarro-Marset (AMAST, 2010)

A Dependency Pair Framework for A OR C-Termination. - Beatriz Alarcón; Salvador Lucas; José Meseguer 001 (WRLA, 2010)

Proving Termination in the Context-Sensitive Dependency Pair Framework. - Raúl Gutiérrez; Salvador Lucas (WRLA, 2010)

Context-sensitive dependency pairs. - Beatriz Alarcón; Raúl Gutiérrez; Salvador Lucas (Inf. Comput., 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)

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. - Cristina Borralleras; Salvador Lucas; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (J. Autom. Reason., 2012)

Using Representation Theorems for Proving Polynomials Non-negative. - Salvador Lucas (AISC, 2014)

Models for Logics and Conditional Constraints in Automated Proofs of Termination. - Salvador Lucas; José Meseguer 001 (AISC, 2014)

Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems. - Salvador Lucas; José Meseguer 001; Raúl Gutiérrez (LOPSTR, 2014)

Proving Operational Termination of Declarative Programs in General Logics. - Salvador Lucas; José Meseguer 001 (PPDP, 2014)

Strong and Weak Operational Termination of Order-Sorted Rewrite Theories. - Salvador Lucas; José Meseguer 001 (WRLA, 2014)

2D Dependency Pairs for Proving Operational Termination of CTRSs. - Salvador Lucas; José Meseguer 001 (WRLA, 2014)

Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting. - Raúl Gutiérrez; Salvador Lucas (Logic, Rewriting, and Concurrency, 2015)

Localized Operational Termination in General Logics. - Salvador Lucas; José Meseguer 001 (Software, Services, and Systems, 2015)

Termination of canonical context-sensitive rewriting and productivity of rewrite systems. - Salvador Lucas (PROLE, 2015)

Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving. - Salvador Lucas (PROLE, 2015)

Completeness of context-sensitive rewriting. - Salvador Lucas (Inf. Process. Lett., 2015)

Use of Logical Models for Proving Operational Termination in General Logics. - Salvador Lucas (WRLA, 2016)

Normal forms and normal theories in conditional rewriting. - Salvador Lucas; José Meseguer 001 (J. Log. Algebraic Methods Program., 2016)

Analysis of Rewriting-Based Systems as First-Order Theories. - Salvador Lucas (LOPSTR, 2017)

A Semantic Approach to the Analysis of Rewriting-Based Systems. - Salvador Lucas (CoRR, 2017)

Dependency pairs for proving termination properties of conditional term rewriting systems. - Salvador Lucas; José Meseguer 001 (J. Log. Algebraic Methods Program., 2017)

Proving Program Properties as First-Order Satisfiability. - Salvador Lucas (LOPSTR, 2018)

Use of logical models for proving infeasibility in term rewriting. - Salvador Lucas; Raúl Gutiérrez (Inf. Process. Lett., 2018)

Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories. - Salvador Lucas; Raúl Gutiérrez (J. Autom. Reason., 2018)

The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors. - Salvador Lucas; José Meseguer 001; Raúl Gutiérrez (J. Comput. Syst. Sci., 2018)

Automatic Generation of Logical Models with AGES. - Raúl Gutiérrez; Salvador Lucas (CADE, 2019)

Proving semantic properties as first-order satisfiability. - Salvador Lucas (Artif. Intell., 2019)

Automatically Proving and Disproving Feasibility Conditions. - Raúl Gutiérrez; Salvador Lucas (IJCAR (2), 2020)

mu-term: Verify Termination Properties Automatically (System Description). - Raúl Gutiérrez; Salvador Lucas (IJCAR (2), 2020)

Proving Semantic Properties as First-Order Satisfiability (Extended Abstract). - Salvador Lucas (IJCAI, 2020)

Using Well-Founded Relations for Proving Operational Termination. - Salvador Lucas (J. Autom. Reason., 2020)

The 2D Dependency Pair Framework for Conditional Rewrite Systems - Part II: Advanced Processors and Implementation Techniques. - Salvador Lucas; José Meseguer 001; Raúl Gutiérrez (J. Autom. Reason., 2020)

Confluence of Conditional Rewriting in Logic Form. - Raúl Gutiérrez; Salvador Lucas; Miguel Vítores (FSTTCS, 2021)

Context-sensitive Rewriting. - Salvador Lucas (ACM Comput. Surv., 2021)

Derivational Complexity and Context-Sensitive Rewriting. - Salvador Lucas (J. Autom. Reason., 2021)

Applications and extensions of context-sensitive rewriting. - Salvador Lucas (J. Log. Algebraic Methods Program., 2021)

The origins of the halting problem. - Salvador Lucas (J. Log. Algebraic Methods Program., 2021)

Confluence Framework: Proving Confluence with CONFident. - Raúl Gutiérrez; Miguel Vítores; Salvador Lucas (LOPSTR, 2022)

Proving and disproving confluence of context-sensitive rewriting. - Salvador Lucas; Miguel Vítores; Raúl Gutiérrez (J. Log. Algebraic Methods Program., 2022)

Confluence of Conditional Rewriting Modulo. - Salvador Lucas (CSL, 2024)

Termination of Generalized Term Rewriting Systems. - Salvador Lucas (FSCD, 2024)

Proving Confluence in the Confluence Framework with CONFident. - Raúl Gutiérrez; Salvador Lucas; Miguel Vítores (Fundam. Informaticae, 2024)

Local confluence of conditional and generalized term rewriting systems. - Salvador Lucas (J. Log. Algebraic Methods Program., 2024)

Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems. - Salvador Lucas (CADE, 2025)