The Conservation Theorem revisited

This paper describes a method of proving strong normalization based on an extension of the conservation theorem. We introduce a structural notion of reduction that we call βS, and we prove that any λ-term that has a βI βS-normal form is strongly β-normalizable. We show how to use this result to prove the strong normalization of different typed λ-calculi.

• Type: Conference
• Year: 1993
• Where: TLCA
• Authors: Philippe de Groote
• Keywords: Conservation Theorem, Strong Normalization, Structural Notion, Theoretical Computer Science, TLCA 1993