| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Jean-Jacques Lévy
Date: April 1991
Summary: Can strong normalization of the typed lambda calculus be proved by a reasonably straightforward mapping from typed terms to a well-founded ordering?
Can strong normalization (termination) of the typed lambda calculus be proved by a reasonably straightforward mapping from typed terms to a well-founded ordering? Note that the type structure can remain unchanged by β-reduction. The same question arises with polymorphic (second-order) lambda calculus.
| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |