Skip to Main content Skip to Navigation
New interface
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
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Saturday, September 8, 2012 - 7:11:52 PM
Last modification on : Friday, February 4, 2022 - 3:08:34 AM
Long-term archiving on: : Sunday, December 9, 2012 - 3:37:33 AM


Publisher files allowed on an open archive




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⟩



Record views


Files downloads