[research interests]
[term rewriting]
Term rewriting is a branch of theoretical computer science which combines elements of logic, universal algebra, automated theorem proving and functional programming. Its foundation is equational logic. What distinguishes term rewriting from equational logic is that equations are used as directed replacement rules, i.e. the left-hand side can be replaced by the right-hand side, but not vice versa. This constitutes a Turing-complete computational model which is very close to functional programming.
F. Bader and T. Nipkow. Term Rewriting and All That. Cambridge University Press. 1998.
[functional programming]
Functional programming is a programming paradigm that conceives computation as the evaluation of mathematical functions and avoids state and mutable data. Functional programming emphasizes the application of functions, in contrast with imperative programming, which emphasizes changes in state and the execution of sequential commands.
P. Hudak. Conception, evolution, and application of functional programming languages. ACM Computing Surveys 21 (3): 359-411. 1989
[publications]
2012
Order-Sorted Equality Enrichments Modulo Axioms
with C. Rocha and J. Meseguer
In F. Durán, editor, Proc. of the 9th International Workshop on Rewriting, WRLA'12, to appear, 2012.
< abstract | download | BibTeX entry >
2011
Proving Termination Properties with MU-TERM
with B. Alarcón, S. Lucas and R. Navarro-Marset
In M. Johnson and D. Pavlovic, editors, Proc. of the 13th International Conference on Algebraic Methodology And Software Technology, AMAST'10, volumen 6486 of LNCS, pages 201-208, 2011.
< abstract | download | BibTeX entry >
2010
Automatic Proofs of Termination of Context-Sensitive Rewriting
PhD. Thesis, Departament de Sistemes Informàtics i Computació, Universitat Politècnica de València, Valencia, Spain, 2010.
© DSIC
< abstract | download | BibTeX entry >
Proving Termination in the Context-Senstive Dependency Pair Framework
with S. Lucas
In P. Ölveczky, editor, Proc. of the 8th International Workshop on Rewriting, WRLA'10, volume 6381 of LNCS, pages 19-35, 2010.
< abstract | download | BibTeX entry >
Proving Termination in the Context-Senstive Dependency Pair Framework
with S. Lucas
Technical Report DSIC-II/02/10 (27 pages). Departmento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, February 2010.
< abstract | download | BibTeX entry >
Context-Sensitive Dependency Pairs
with B. Alarcón and S. Lucas
Information and Computation, 208:922-968, 2010.
© Elsevier
< abstract | download | BibTeX entry >
2009
Mechanizing Proofs of Termination in the Context-Sensitive Dependency Pair Framework
with S. Lucas
In P. Lucio, G. Moreno and R. Peña, editors, Proc. of the 9th Spanish Conference on Programming and Languages, PROLE'09, pages 265-274, 2009.
< abstract | download | BibTeX entry >
Mechanizing Proofs of Termination with Context-Sensitive Dependency Pairs
with S. Lucas
In A. Geser and J. Waldmann, editors, Proc. of the 10th International Workshop on Termination, WST'09, pages 12-15, 2009.
< abstract | download | BibTeX entry >
Non-Collapsing Context-Sensitive Dependency Pairs
with B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, S. Lucas, P. Schneider-Kamp and R. Thiemann
In A. Geser and J. Waldmann, editors, Proc. of the 10th International Workshop on Termination, WST'09, pages 8-11, 2009.
< abstract | download | BibTeX entry >
2008
Improving Context-Sensitive Dependency Pairs
with B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, S. Lucas, P. Schneider-Kamp and R. Thiemann
In I. Cervesato, H. Veith and A. Voronkov, editors, Proc. of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR'08, volume 5330 of LNCS, pages 636-651, 2008.
< abstract | download | BibTeX entry >
Improving Context-Sensitive Dependency Pairs
with B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, S. Lucas, P. Schneider-Kamp and R. Thiemann
Technical Report AIB 2008-13 (29 pages). Department of Computer Science, RWTH Aachen University, Germany, June 2008.
< abstract | download | BibTeX entry >
Usable Rules for Context-Sensitive Rewrite Systems
with S. Lucas and X. Urbain
In A. Voronkov, editor, Proc. of the 19th International Conference on Rewriting Techniques and Applications, RTA'08, volume 5117 of LNCS, pages 126-141, 2008.
< abstract | download | BibTeX entry >
Usable Rules for Context-Sensitive Rewrite Systems
with S. Lucas and X. Urbain
Technical Report DSIC-II/03/08 (23 pages). Departmento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, April 2008.
< abstract | download | BibTeX entry >
2007
Towards a notion of Usable Rule for Context-Sensitive Rewrite Systems
with S. Lucas and X. Urbain
In E. Pimentel, editor, Proc. of the 7th Spanish Conference on Programming and Languages, PROLE'07, pages 243-252, 2007.
< abstract | download | BibTeX entry >
Improving Termination Proofs of Context-Sensitive Rewriting using Dependency Pairs
with B. Alarcón and S. Lucas
In D. Hofbauer and A. Serebrenik, editors, Proc. of the 9th Workshop of Termination, WST'07, pages 22-25, 2007.
< abstract | download | BibTeX entry >
Improving the Context-Sensitive Dependency Graph
with B. Alarcón and S. Lucas
ENTCS, volume 188, pages 91-103, 2007.
© Elsevier
< abstract | download | BibTeX entry >
Proving Termination of Context-Sensitive Rewriting with MU-TERM
with B. Alarcón, J. Iborra and S. Lucas
ENTCS, volume 188, pages 105-115, 2007.
© Elsevier
< abstract | download | BibTeX entry >
2006
Context-Sensitive Dependency Pairs
with B. Alarcón and S. Lucas
In S. Arun-Kumar and N.Garg, editors, Proc. of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'06, volume 4437 of LNCS, pages298-309, 2006.
< abstract | download | BibTeX entry >
Dependency Pairs for Context-Sensitive Rewriting
with B. Alarcón and S. Lucas
Technical Report DSIC II/07/06 (24 pages). Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, June 2006.
< abstract | download | BibTeX entry >
Proving Termination of Context-Sensitive Rewriting with MU-TERM
with B. Alarcón, J. Iborra and S. Lucas
In P. Lucio, editor, Proc. of the 4th Spanish Conference on Programming and Languages, PROLE'06, volume I, pages 107-118, 2006.
© CIMNE Barcelona
< abstract | download | BibTeX entry >
Towards a Dependency Pair Framework for Context-Sensitive Rewriting
with B. Alarcón and S. Lucas
In P. Lucio, editor, Proc. of the 4th Spanish Conference on Programming and Languages, PROLE'06, volume I, pages 77-86, 2006.
© CIMNE Barcelona
< abstract | download | BibTeX entry >
2005
Genetic Algorithms using Parallelism and FPGAs: The TSP as Case Study
with M. A. Vega Rodríguez and J. M. Ávila Román, J. M. Sánchez Pérez, J. A. Gómez Pulido
Proc. of 34th International Conference on Parallel Processing, ICPP'05, 0:573-579, 2005.
© IEEE
< abstract | download | BibTeX entry >
2004
Implementación Hardware de Algoritmos Genéticos usando FPGAs: El TSP como Caso de Estudio
with M. A. Vega Rodríguez and J. M. Ávila Román, J. M. Sánchez Pérez, J. A. Gómez Pulido
FPGAs: Computación & Aplicaciones. Proc. of the 4th Jornadas de Computación Reconfigurable y Aplicaciones, JCRA'04, pages 155-162, 2004.
< abstract | download | BibTeX entry >
