Type theory and rewriting. F. Blanqui. Ph.D. thesis, University Paris-Sud, 139 pages, 2001. Version en français. SPECIF 2001 PhD thesis award.

Erratum

p41. In Lemma 33, for C to preserve sorts, we need sorts to be irreducible by →.

p50. In Lemma 54, → needs to preserve typing in ⊢g.

Statcounter W3C Validator Last updated on 22 April 2023. Come back to main page.