Advanced
Weak Normalization
A proof of weak head normalization for the simply typed lambda calculus using logical relations.
Normalization by Evaluation
A proof of weak head normalization for the simply typed lambda calculus using logical relations.