| Created on: May 26, 2005 |
| Last update: May 10, 2006 |
HORPO
(The Higher Order Recursive Path Ordering)
[ About HORPO | News | Download | Relevant publications ]
Dershowitz' recursive path ordering (RPO) is one of the important methods for proving termination of term rewrite systems (TRSs). J.-P. Jouannaud and A. Rubio proposed its generalization for the higher-order case giving rise to HORPO: Higher-order recursive path ordering.
This project's goal is the formalization of the HORPO ordering in the proof checker Coq.
This formalization is part of CoLoR: the Coq Library on Rewriting and Termination. Color's ultimate goal is to certify termination proofs produced by tools like AProVE, Cime, Matchbox, TORPA, TPA, TTT. For that purpose first the theory behind existing termination techniques (like RPO) has to be formalized.
The formalization of HORPO is complete (axiom-free) and fully constructive. The main result states that union of the HORPO ordering and the beta-reduction relation of the simply typed lambda calculus is well-founded. Simply typed lambda calculus is used as a meta language in higher-order rewriting and multisets are used for comparison of arguments is the HORPO ordering so they had to be formalized as well. The formalization contains around 25.000 lines of Coq scripts at the moment. It roughly consists of the following three parts (see publications for more details):
| 10.05.2006 | New release of CoLoR including HORPO is available! |
|---|---|
| 27.04.2006 | The HORPO project has been merged into CoLoR. A new release of CoLoR containing HORPO should be available any moment now! |
| 23.02.2006 | The work on the development has been finished! See the Browse & Download section. |
| 05.2005 | Master's Thesis concerning HORPO printed as a Technical Report at VU (check publications section). |
| 26.05.2005 | Web-page of HORPO launched! |
| 09.07.2004 | Presentation by Femke van Raamsdonk of RPO (by Nicole de Kleijn) and HORPO during Dutch Proof Tools Day 2004. |
| 01.2004 | Work on HORPO - my Master's project at Vrije Universiteit, Amsterdam- starts. |
Now that this work has become part of CoLoR project you can download it from CoLoR webpage.
You can also browse the content of CoLoR. The different parts of this development can be found in:
You can see all of my publications here.
Description of the formalization with focus on HORPO.
Adam Koprowski
Certified Higher-Order Recursive Path Ordering.
In Proceedings of the 17th International Conference on Rewriting Techniques and Applications, (RTA '06), Seattle, WA, USA. (To appear)
Get: see my publications page
Description of the part of the formalization dealing with simply typed lambda terms.
Adam Koprowski
A Formalization of the Simply Typed Lambda Calculus in Coq.
Submitted.
Get: see my publications page
Early description of HORPO.
Adam Koprowski
Well-foundedness of the Higher Order Recursive Path Ordering in Coq.
Master's Thesis printed as Technical Report TI-IR-004, Department of Theoretical Computer Science, Vrije Universiteit, Amsterdam, The Netherlands
Get: see my publications page
Extensions of HORPO - partly subject of formalization.
Jean-Pierre Jouannaud and Albert Rubio
Higher-Order Recursive Path Orderings à la carte.
Invited lecture In Workshop on Termination, The Netherlands, 2001.
Get: see J.-P.Jouannaud's page
The definition and the proof of well-foundedness of HORPO - subject of formalization.
Jean-Pierre Jouannaud and Albert Rubio
The Higher-Order Recursive Path Ordering.
IEEE Symposium on Logic in Computer Science, Trento, Italy, July 1999.
Get: see J.-P.Jouannaud's page
Description of RPO (by Nicole de Kleijn) and HORPO.
Nicole de Kleijn, Adam Koprowski and Femke van Raamsdonk
Well-foundedness of the Recursive Path Ordering in Coq.
In Dutch Proof Tools Day 2004, Program + Proceedings, University of Nijmegen, Nijmegen, The Netherlands, July 2004
Get: see my publications page
[ About HORPO | News | Download | Relevant publications ]
|
|
|