Church-Rosser Properties of Normal Rewriting
Résumé
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.
Fichier principal
paper27.pdf (363.47 Ko)
Télécharger le fichier
presentation-CSL.pdf (131.76 Ko)
Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Format : Autre