Refinement Types as Higher-Order Dependency Pairs

Cody Roux
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...
This data center is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.
We found no citations for this text. For information on how to provide citation information, please see our documentation.