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.