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).
Type de document :
Communication dans un congrès
18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal. 2009
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00397689
Contributeur : Frédéric Blanqui <>
Soumis le : mardi 23 juin 2009 - 06:19:24
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mardi 15 juin 2010 - 17:25:21

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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

Collections

Citation

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. 2009. 〈inria-00397689〉

Partager

Métriques

Consultations de la notice

412

Téléchargements de fichiers

163