HOR  2007

4th International Workshop on Higher-Order Rewriting

Monday June 25, 2007          Paris, France

Topics - Call for Abstracts - Invited Speakers - Submissions - Program - Dates - Proceedings - Program Committee - Steering Committee - Local Arrangements

HOR 2007 is a forum to present work concerning all aspects of higher-order rewriting. The aim is to provide an informal and friendly setting to discuss recent work and work in progress.

HOR 2002 was part of FLoC 2002 in Copenhagen, Denmark.

HOR 2004 was part of the RDP 2004 in Aachen, Germany.

HOR 2006 was part of FLoC 2006 in Seattle, USA.

HOR 2007 is part of RDP 2007 in Paris, France.

This year, HOR enjoys additionally the status of a "small workshop" of the TYPES project.

There will also be a "small TYPES workshop" on Type theory, proof theory and rewriting (TPR '07), 4 days later in Paris.


HOR 2007 is a forum to present work concerning all aspects of higher-order rewriting. The following is a non-exhaustive list of topics for the workshop:  

Abstracts between 2 and 5 pages. As HOR is meant to be a platform to discuss ongoing research we are also interested in abstracts describing work in progress, or problems in higher-order rewriting. Please use the submission web site http://www.easychair.org/HOR2007/ (CLOSED). Please address your questions to the PC chair, under family_name@irit.fr.


Note: Kristoffer Rose could not come to the workshop. He provided material to be presented in his absence, but technical problems did not make this possible. Please find the material on his personal page http://www.krisrose.net. A local copy of his slides for the talk and the 54,7MB and 35 minutes AVI talk presentation with voice (slides run a bit behind the voice; after minute 26, this should be taken into account). Finally, the AVI demo presentation with voice (38,9MB and 19 minutes).

Carsten Schürmann    IT University of Copenhagen, Denmark   On the formalization of logical relation arguments in Twelf
Tarmo Uustalu    Institute of Cybernetics, Tallinn University of Technology, Estonia   Circular proofs = Mendler in sequent form

Andreas Abel    Syntactical strong normalization for intersection types with term rewriting rules
Lisa Allali    Algorithmic equality in Heyting arithmetic modulo
Takahito Aoto and Toshiyuki Yamada    Argument filterings and usable rules for simply typed dependency pairs
Lionel Marie-Magdeleine and Serguei Soloviev    Non-standard reductions in simply-typed, higher order and dependently-typed systems
Kristoffer Rose    CRSX - an open source platform for experiments with higher-order rewriting
Max Schäfer    Elements of a categorical semantics for the Open Calculus of Constructions
Daniel Ventura, Mauricio Ayala-Rincon and Fairouz Kamareddine    Principal typings for explicit substitutions calculi

Kristoffer Rose    Demonstration of CRSX


Submission Deadline (extended):   Friday, April 27, 2007
Notification (delayed by 4 days due to the extension):   Tuesday, May 15, 2007
Final Version:   Monday, June 4, 2007


The PDF proceedings of HOR 2007 are here, and copies have been distributed to the participants at the workshop.


Herman Geuvers    Radboud University Nijmegen   The Netherlands
Makoto Hamana    Gunma University   Japan
Ralph Matthes (chair)    C.N.R.S., University of Toulouse III   France
Albert Rubio    Technical University of Catalonia   Spain
Mark-Oliver Stehr    SRI International   USA


Delia Kesner    Université Paris 7   France
Femke van Raamsdonk    Vrije Universiteit   The Netherlands


The organizers of RDP 2007 (Antonio Bucciarelli, Vincent Padovani, Ralf Treinen, Xavier Urbain).