Refinement Types as Higher-Order Dependency Pairs

Reference. Refinement Types as Higher-Order Dependency Pairs

Cody Roux · RTA · 2011 · refinement-types · DOI · arXiv

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.

Cite

Cite as @roux-2011-refinement (helia, typst) · \cite{roux-2011-refinement} (LaTeX)

BibTeX

bibtex · 14 lines

@inproceedings{roux-2011-refinement,
  doi = {10.4230/LIPICS.RTA.2011.299},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.299},
  author = {Roux, Cody},
  keywords = {Dependency Pairs, Higher-Order, Refinement Types},
  language = {en},
  title = {Refinement Types as Higher-Order Dependency Pairs},
  volume = {10},
  pages = {299-312},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2011},
  copyright = {Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license},
  booktitle = {22nd International Conference on Rewriting Techniques and Applications (RTA'11)}
}

hayagriva YAML (typst)

yaml · 14 lines

roux-2011-refinement:
  type: article
  title: Refinement Types as Higher-Order Dependency Pairs
  author: Roux, Cody
  date: 2011
  page-range: 299-312
  url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.299
  serial-number:
    doi: 10.4230/LIPICS.RTA.2011.299
  parent:
    type: proceedings
    title: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
    volume: 10

Download: roux-2011-refinement.bib · roux-2011-refinement.yml

Cites 32 works (2 here)

With notes (2)

On the Relation between Sized-Types Based Termination and Semantic Labelling blanqui-2009-onCSL · 2009

DOI · arXiv

Dependent types in practical programming xi-1999-dependentPOPL · 1999

PDF · DOI · pldb

External (30)

Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems (2009)
The Coq Reference Manual, Version 8.2 (2008)
Liquid types (2008)
Towards a practical programming language based on dependent type theory (2007)
Mechanizing and Improving Dependency Pairs (2007)
Incremental construction of unification algorithms in equational theories (2006)
Semi-continuous Sized Types and Termination (2006)
Why dependent types matter (2006)
Higher-order dependency pairs (2006)
Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems (2006)
Simple unification-based type inference for GADTs (2006)
Proving and Disproving Termination of Higher-Order Functions (2005)
On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems (2005)
Dependency Pairs for Simply Typed Term Rewriting (2005)
Continuous Semantics for Strong Normalization (2005)
Termination checking with types (2004)
Type-based termination of recursive definitions (2004)
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems (2004)
Modular Termination Proofs for Rewriting Using Dependency Pairs (2002)
Inductive-data-type systems (2002)
Defunctionalization at work (2001)
Calculating Sized Types (2001)
The size-change principle for program termination (2001)
Termination of term rewriting using dependency pairs (2000)
Henk: a typed intermediate language (1997)
Proving the correctness of reactive systems using sized types (1996)
Refinement types for ML (1991)
Lambda lifting: Transforming programs to recursive equations (1985)
A theory of type polymorphism in programming (1978)
The mathematical language AUTOMATH, its usage, and some of its extensions (1970)