LIPIcs.CSL.2012.350.pdf
- Filesize: 434 kB
- 16 pages
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.
Feedback for Dagstuhl Publishing