Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00730271
Contributor : Jean-Pierre Jouannaud <>
Submitted on : Saturday, September 8, 2012 - 7:11:52 PM
Last modification on : Tuesday, March 17, 2020 - 2:46:20 AM
Long-term archiving on: : Sunday, December 9, 2012 - 3:37:33 AM

Files

paper27.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

Jean-Pierre Jouannaud, Jian-Qi Li. Church-Rosser Properties of Normal Rewriting. Computer Science Logic, European Association for Computer Science Logic, Sep 2012, Fontainebleau, France. pp.350-365, ⟨10.4230/LIPIcs.CSL.2012.i⟩. ⟨hal-00730271⟩

Share

Metrics

Record views

480

Files downloads

218