RESEARCH

I'm working on Second-Order Unification, mainly in Context and Linear second-order Unification. I'm also working on CSP and logic techniques.

Software:

• SIMPLY: a compiler for a high level CSP modeling language to SAT Modulo Theories
• TILC: the interactive lambda calculus tracer

Papers:

1. Jordi Levy and Mateu Villaret (2009). Simplifying the Signature In Second-Order Unification.
   to appear In Aplicable Algebra in Engineering, Communication and Computing (AAECC).
2. Temur Kutsia, Jordi Levy and Mateu Villaret (2009). On the Relation Between Context and Sequence Unification.
   to appear in Journal on Symbolic Computation (JSC) .
3. Jordi Levy, Manfred Schmidt-Schauss and Mateu Villaret (2009). On The Complexity of Bounded Second-Order Unification and Stratified Context Unification.
   to appear in Journal of Algorithms in Cognition, Informatics, and Logic (JACIL).
4. Beatriz López, Víctor Muñoz, Javier Murillo, Federico Barber, Miguel A. Salido, Montserrat Abril, Mariamar Cervantes, Luis F. Caro and Mateu Villaret. (2009). Experimental analysis of optimization techniques on the road passenger transportation problem.
   Engineering Application of Artificial Intelligence (EAAI) . Volume 22, pages 374-388.
5. David Ruíz and Mateu Villaret (2009). TILC: The Interactive Lambda-Calculus Tracer.
   in Electronic Notes in Theoretical Computer Science (ENTCS) . Volume 248, pages 173-183.
   Proceedings of the Eighth Spanish Conference on Programming and Computer Languages (PROLE 2008)

6. Jordi Levy, Manfred Schmidt-Schauss and Mateu Villaret (2008). The Complexity of Monadic Second-Order Unification.
   In SIAM Journal on Computing. Volume 38, number 3, pages 1113-1140.
7. Jordi Levy and Mateu Villaret (2008). Nominal Unification from a Higher-order Perspective.
   In Proceedings of the 19th Int.Conf. on Rewriting Techniques and Applications, RTA'08. Hagenberg, Austria, July 15-17, 2008.
   Volume 5117 of Lecture Notes in Computer Science, pages 246-260, Springer-Verlag. (Slides).

8. Temur Kutsia, Jordi Levy and Mateu Villaret (2007). Sequence Unification Through Currying.
   In Proceedings of the 18th Int.Conf. on Rewriting Techniques and Applications, RTA'07. Paris, France, June 26-28, 2007.
   Volume 4533 of Lecture Notes in Computer Science, pages 288-302, Springer-Verlag. (Slides).

9. Jordi Levy, Manfred Schmidt-Schauss and Mateu Villaret (2006). Bounded Second-Order Unification Is NP-Complete.
   In Proceedings of the 17th Int.Conf. on Rewriting Techniques and Applications, RTA'06. Seattle, WA, USA, August 12-14, 2006.
   Volume 4098 of Lecture Notes in Computer Science, pages 400-414, Springer-Verlag.

10. Jordi Levy, Manfred Schmidt-Schauss and Mateu Villaret (2006). Stratified Context Unification is NP-complete.
    In Proceedings of the 3rd International Joint Conference on Automated Reasoning, IJCAR'06. Seattle, WA, USA, August 17 - 20, 2006.
    Volume 4130 of Lecture Notes in Artificial Intelligence, pages 82-96, Springer-Verlag.

11. Jordi Levy, Joachim Niehren and Mateu Villaret (2005). Well-Nested Context Unification.
    In Proceedings of the 20th Int. Conference on Automated Deduction, CADE-20. Tallinn, Estonia, July 22-27, 2005.
    Volume 3632 of Lecture Notes in Artificial Intelligence, pages 149-163, Springer-Verlag.

12. Joachim Niehren and Mateu Villaret (2005). Describing Lambda-Terms in Context Unification. (see ICOS-4, below)
    In Proceedings of the 5th. Int Conf. on Logical Aspects of Computational Linguistics, LACL’05. Bordeaux, France, April 2005.
    Volume 3492 of Lecture Notes in Artificial Intelligence, pages 221-237, Springer-Verlag.

13. Jordi Levy, Manfred Schmidt-Schauss and Mateu Villaret (2004). Monadic Second-Order Unification is NP-Complete.
    In Proceedings of the 15th Int. Conf. on Rewriting Techniques and Applications, RTA'04. Aachen, Germany, June 3-5, 2004.
    Volume 3091 of Lecture Notes in Computer Science, pages 55-69, Springer-Verlag. (BPA).

14. Mateu Villaret (2004). On Some Variants of Second-Order Unification.
    Ph. D. Thesis (Slides).
    June 2004, Supervised by Jordi Levy
    Thesis Comitee: Albert Rubio, Guillem Godoy, Philippe de Groote, Joachim Niehren and Manfred Schmidt-Schauss

15. Joachim Niehren and Mateu Villaret (2003). Describing Lambda-Terms in Context Unification.
    In 4th Workshop on Inference in Computational Semantics ICOS-4. Nancy, France, September 2003. (Slides).

16. Joachim Niehren and Mateu Villaret (2002). Parallelism and Tree Regular Constraints.
    In Proceedings of the 9th Int.l Conf. on Logic for Programming Artificial Intelligence and Reasoning, LPAR'02. Tiblissi, Georgia, October 2002.
    Volume 2514 of Lecture Notes in Artficial Intelligence, pages 311-326, Springer-Verlag

17. Mateu Villaret (2002). Processing Tree Regular Constraints in Context Unification.
    In Proceedings of the 7th Student Session of the European Summer School in Logic, Language, and Information, ESSLLI'02. Trento, Italy, August 2002.
    Pages 271-283. (Slides).

18. Jordi Levy and Mateu Villaret (2002). Currying Second-Order Unification Problems.
    In Proceedings of the 13th Int. Conf. on Rewriting Techniques and Applications, RTA'02. Copenhagen, Denmark, July 22-24, 2002.
    Volume 2378 of Lecture Notes in Computer Science, pages 326-339, Springer-Verlag.

19. Jordi Levy and Mateu Villaret (2001). Context Unification and Traversal Equations.
    In Proceedings of the 12th Int. Conf. on Rewriting Techniques and Applications, RTA'01. Utrecht, The Netherlands, May 22-24, 2001.
    Volume 2051 of Lecture Notes in Computer Science, pages 169-184, Springer-Verlag.

20. Jordi Levy and Mateu Villaret (2000). Linear Second-Order Unification and Context Unification with Tree-Regular Constraints.
    In Proceedings of the 11th Int. Conf. on Rewriting Techniques and Applications, RTA'00. Norwich, UK, July 10-12, 2000.
    Volume 1833 of Lecture Notes in Computer Science, pages 156-171, Springer-Verlag. (Slides).

21. Jordi Levy and Mateu Villaret (1998). Complexity Study of some Classes of Context and Second-Order Unification Problems.
    Twelfth Int. Workshop on Unification, UNIF'98. Rome, Italy. (Slides).

Research events:

• TPF’10 Segundo Taller de Programación Funcional (workshop de PROLE’10)
• TPF'09 Primer Taller de Programación Funcional (workshop de PROLE'09).
• UNIF'06 collocated with FLOC'06 in Seatle, USA.
• UNIF'03 collocated with RDP'03 in Valencia, Spain.

A link to Journals, conferences, papers... Computer Science Bibliography