Church-Rosser Properties of Normal Rewriting

Jean-Pierre Jouannaud 1 Jian-Qi Li 1
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : We prove a general purpose abstract Church-Rosser result that captures most existing such results that rely on termination of computations. This is achieved by studying abstract normal rewriting in a way that allows to incorporate positions at the abstract level. New concrete Church- Rosser results are obtained, in particular for higher-order rewriting at higher types.
Type de document :
Communication dans un congrès
Patrick Cégielsky and Arnaud Durand. Computer Science Logic, Sep 2012, Fontainebleau, France. Dagstuhl Publishing, 16, pp.350-365, 2012, LIPIcs. 〈10.4230/LIPIcs.CSL.2012.i〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00730271
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : samedi 8 septembre 2012 - 19:11:52
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : dimanche 9 décembre 2012 - 03:37:33

Fichiers

paper27.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Jean-Pierre Jouannaud, Jian-Qi Li. Church-Rosser Properties of Normal Rewriting. Patrick Cégielsky and Arnaud Durand. Computer Science Logic, Sep 2012, Fontainebleau, France. Dagstuhl Publishing, 16, pp.350-365, 2012, LIPIcs. 〈10.4230/LIPIcs.CSL.2012.i〉. 〈hal-00730271〉

Partager

Métriques

Consultations de la notice

263

Téléchargements de fichiers

131