¶Abstract

We present a new proof of the standardization theorem in λ-calculus, which is performed by inductions based on an inductive definition of β-reducibility with a standard sequence.