Termination of rewrite relations on λ-terms based on Girard's notion of reducibility. F. Blanqui. TCS 611, 37 pages, 2016.

Erratum

p. 53, l. 25 (stable subterm). After "FV(t)⊆FV(u)", add: " and no bound variable of u belongs to FV(t)".

p. 56, l. -12. Replace "Sat: Tait' set of saturated sets [Tai75]" by "Sat: Mitchell' set of type sets relative to SN [Mit86] (called saturated in [Gal90])", with [Mit86] J. Mitchell. A type-inference approach to reduction properties and semantics of polymorphic expressions (summary). In the proceedings of the ACM Symposium on Lisp and Fonctional Programming, 1986.

p. 58, l. -15. Replace "Π_x∈AB_x = P(Σ_x∈AB_x)" by "Π_x∈AB_x ⊆ P(Σ_x∈AB_x)".

Last updated on 27 April 2024. Come back to main page.