Skip to Main content Skip to Navigation
Conference papers

On the relation between sized-types based termination and semantic labelling

Frédéric Blanqui 1 Cody Roux 2 
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
2 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We investigate the relationship between two independently developed termination techniques. On the one hand, sized-types based termination (SBT) uses types annotated with size expressions and Girard's reducibility candidates, and applies on systems using constructor matching only. On the other hand, semantic labelling transforms a rewrite system by annotating each function symbol with the semantics of its arguments, and applies to any rewrite system. First, we introduce a simplified version of SBT for the simply-typed lambda-calculus. Then, we give new proofs of the correctness of SBT using semantic labelling, both in the first and in the higher-order case. As a consequence, we show that SBT can be extended to systems using matching on defined symbols (e.g. associative functions).
Document type :
Conference papers
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Tuesday, June 23, 2009 - 6:19:24 AM
Last modification on : Friday, January 21, 2022 - 3:19:06 AM
Long-term archiving on: : Tuesday, June 15, 2010 - 5:25:21 PM


Files produced by the author(s)


  • HAL Id : inria-00397689, version 1
  • ARXIV : 0906.4173



Frédéric Blanqui, Cody Roux. On the relation between sized-types based termination and semantic labelling. 18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal. ⟨inria-00397689⟩



Record views


Files downloads