文章基本信息

标题：Refinement Types as Higher-Order Dependency Pairs
本地全文：下载
作者：Cody Roux
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2011
卷号：10
页码：299-312
DOI：10.4230/LIPIcs.RTA.2011.299
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Dependency Pairs; Higher-Order; Refinement Types