opening [research activities] ... done.

[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.

© Springer-Verlag


< 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.

© Springer-Verlag


< 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.

© Springer-Verlag


< 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.

© Springer-Verlag


< 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.

© Springer-Verlag


< 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.

© Springer-Verlag


< 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 >

Foot image