Refinement Types as Higher Order Dependency Pairs
Logic in Computer Science
2011-01-25 v2
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 object of active research. We observe that a variant of refinement types allow us to express a form of higher-order dependency pair criterion that only uses information at the type level, and we prove the correctness of this criterion.
Cite
@article{arxiv.1101.0968,
title = {Refinement Types as Higher Order Dependency Pairs},
author = {Cody Roux},
journal= {arXiv preprint arXiv:1101.0968},
year = {2011}
}