2026-07-23T15:49:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3127 2024-03-06T10:33:52Z ddc:004 open_access

Refinement Types as Higher-Order Dependency Pairs Roux, Cody Dependency Pairs Higher-Order Refinement Types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Cody Roux 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.299 urn:nbn:de:0030-drops-31273 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.299 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode