On the Relation between Sized-Types Based Termination and Semantic Labelling

Reference. On the Relation between Sized-Types Based Termination and Semantic Labelling

Frédéric Blanqui, Cody Roux · CSL · 2009 · DOI · arXiv

Cite

Cite as @blanqui-2009-on (helia, typst) · \cite{blanqui-2009-on} (LaTeX)

BibTeX

bibtex · 1 line

@inbook{blanqui-2009-on, title={On the Relation between Sized-Types Based Termination and Semantic Labelling}, ISBN={9783642040276}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-642-04027-6_13}, DOI={10.1007/978-3-642-04027-6_13}, booktitle={Computer Science Logic}, publisher={Springer Berlin Heidelberg}, author={Blanqui, Frédéric and Roux, Cody}, year={2009}, pages={147–162} }

hayagriva YAML (typst)

yaml · 17 lines

blanqui-2009-on:
  type: chapter
  title: On the Relation between Sized-Types Based Termination and Semantic Labelling
  author:
  - Blanqui, Frédéric
  - Roux, Cody
  date: 2009
  page-range: 147-162
  url: http://dx.doi.org/10.1007/978-3-642-04027-6_13
  serial-number:
    doi: 10.1007/978-3-642-04027-6_13
    isbn: '9783642040276'
    issn: 1611-3349
  parent:
    type: book
    title: Computer Science Logic
    publisher: Springer Berlin Heidelberg

Download: blanqui-2009-on.bib · blanqui-2009-on.yml

Cited by (1)

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.

DOI · arXiv

Cites 22 works (1 here)

With notes (1)

Abstract syntax and variable binding fiore_etal_ndLICS

We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.

DOI

External (21)

On the relation between sized-types based termination and semantic labelling (full version) (2009)
Semi-continuous Sized Types and Termination (2008)
Higher-order semantic labelling for inductive datatype systems (2007)
Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems (2006)
Predictive Labeling (2006)
Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations (2005)
Definitions by rewriting in the Calculus of Constructions (2005)
Universal Algebra for Termination of Higher-Order Rewriting (2005)
Type-based termination of recursive definitions (2004)
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems (2004)
Dependent types for program termination verification (2001)
Termination and Confluence of Higher-Order Rewrite Systems (2000)
On the union of well-founded relations (1998)
Proving the correctness of reactive systems using sized types (1996)
Transforming termination by self-labelling (1996)
Un Calcul de Constructions infinies et son application à la vérification de systèmes communicants (PhD thesis, ENS Lyon) (1996)
TERMINATION OF TERM REWRITING BY SEMANTIC LABELLING (1995)
Combinatory reduction systems: introduction and survey (1993)
A logic programming language with lambda-abstraction, function variables, and simple unification (1991)
Inductive Definition in Type Theory (PhD thesis, Cornell University) (1987)
Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur (PhD thesis, Université Paris VII) (1972)

Cite

Refinement Types as Higher-Order Dependency Pairs roux-2011-refinementRTA · 2011

Abstract syntax and variable binding fiore_etal_ndLICS