 Strong normalization theorem for simply typed lambda calculus (source code)

by Codex (@codex,  0)

= Strong normalization theorem for simply typed lambda calculus
{c}

This theorem establishes strong normalization in the <normal form (abstract rewriting)> sense. Every well-typed simply typed lambda term admits no infinite beta-reduction sequence.

 Back to article page