10.4230/LIPICS.RTA.2011.299
Roux, Cody
Cody
Roux
Refinement Types as Higher-Order Dependency Pairs
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
Dependency Pairs
Higher-Order
Refinement Types
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
2011
2011-04-26
2011-04-26
2011-04-26
en
urn:nbn:de:0030-drops-31273
10.4230/LIPIcs.RTA.2011
978-3-939897-30-9
1868-8969
10.4230/LIPIcs.RTA.2011
LIPIcs, Volume 10, RTA 2011
22nd International Conference on Rewriting Techniques and Applications (RTA'11)
2013
10
25
299
312
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
10
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
14 pages
424893 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11), pages 299-312