Skip to Main content Skip to Navigation
Reports

Refinement Types as Higher Order Dependency Pairs

Cody Roux 1 
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Reports
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00552046
Contributor : Cody Roux Connect in order to contact the contributor
Submitted on : Monday, January 24, 2011 - 5:20:55 PM
Last modification on : Saturday, June 25, 2022 - 7:44:59 PM
Long-term archiving on: : Monday, April 25, 2011 - 3:23:12 AM

Files

roux_ref_dp.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00552046, version 2
  • ARXIV : 1101.0968

Collections

Citation

Cody Roux. Refinement Types as Higher Order Dependency Pairs. [Research Report] 2011, pp.19. ⟨inria-00552046v2⟩

Share

Metrics

Record views

87

Files downloads

101