MIZ-PR: A Theorem Prover for Polymorphic and Recursive Functions. - Javier Leach; Susana Nieva (LPAR, 1992)

Foundations of a theorem prover for functional and mathematical uses. - Javier Leach; Susana Nieva (J. Appl. Non Class. Logics, 1993)

Reasoning with Preorders and Dynamic Sorts Using Free Variable Tableaux. - Antonio Gavilanes; Javier Leach; Pedro J. Martín; Susana Nieva (AISMC, 1996)

Free Variable Tableaux for a Many Sorted Logic with Preorders. - Antonio Gavilanes; Javier Leach; Susana Nieva (AMAST, 1996)

Constraint Logic Programming with Hereditary Harrop Formulas. - Javier Leach; Susana Nieva; Mario Rodríguez-Artalejo (ILPS, 1997)

Free Variable Tableaux for a Logic with Term Declarations. - Pedro J. Martín; Antonio Gavilanes; Javier Leach (TABLEAUX, 1998)

A Higher-Order Programming Language with Constraints. - Javier Leach; Susana Nieva (WFLP, 2000)

Tableau Methods for a Logic with Term Declarations. - Pedro J. Martín; Antonio Gavilanes; Javier Leach (J. Symb. Comput., 2000)

A Higher-Order Logic Programming Language with Constraints. - Javier Leach; Susana Nieva (FLOPS, 2001)

Constraint Logic Programming with Hereditary Harrop Formula. - Javier Leach; Susana Nieva; Mario Rodríguez-Artalejo (Theory Pract. Log. Program., 2001)

A logic programming approach to the verification of functional-logic programs. - José Miguel Cleva; Javier Leach; Francisco Javier López-Fraguas (PPDP, 2004)