Continuous normalization for the lambda-calculus and Gödel's T

Finally, the methods are extended to an infinitary λ-calculus with ω-rule and permutative conversions and this is used to derive a strong form of normalization for an iterative version of Gödel's system T, leading to a value table semantics for number-theoretic functions.