Refinement Types as Higher Order Dependency Pairs

TL;DR

This paper introduces a novel approach that uses refinement types to express higher-order dependency pair criteria, enabling type-level analysis for proving termination of higher-order rewrite systems.

Contribution

It demonstrates how refinement types can be extended to encode higher-order dependency pairs and proves the correctness of this new criterion.

Findings

Refinement types can express higher-order dependency pair criteria.

The proposed criterion is proven correct.

Type-level information suffices for termination analysis.

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.