Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.299
URN: urn:nbn:de:0030-drops-31273
URL: https://drops.dagstuhl.de/opus/volltexte/2011/3127/
Roux, Cody
Refinement Types as Higher-Order Dependency Pairs
| pdf-format: |
|
Abstract
Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of rewrite systems; however its extension to higher-order rewrite systems is still the subject of active research. We observe that a variant of refinement types allows us to express a form of higher-order dependency pair method: from the rewrite system labeled with typing information, we build a type-level approximated dependency graph, and describe a type level embedding preorder. We describe a syntactic termination criterion involving the graph and the preorder, which generalizes the simple projection criterion of Middeldorp and Hirokawa, and prove our main result: if the graph passes the criterion, then every well-typed term is strongly normalizing.
BibTeX - Entry
@InProceedings{roux:LIPIcs:2011:3127,
author = {Cody Roux},
title = {{Refinement Types as Higher-Order Dependency Pairs}},
booktitle = {22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
pages = {299--312},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-30-9 },
ISSN = {1868-8969},
year = {2011},
volume = {10},
editor = {Manfred Schmidt-Schau{\ss}},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3127},
URN = {urn:nbn:de:0030-drops-31273},
doi = {10.4230/LIPIcs.RTA.2011.299},
annote = {Keywords: Dependency Pairs, Higher-Order, Refinement Types}
}
| Keywords: | Dependency Pairs, Higher-Order, Refinement Types | |
| Seminar: | 22nd International Conference on Rewriting Techniques and Applications (RTA'11) | |
| Issue date: | 2011 | |
| Date of publication: | 26.04.2011 |
