## 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.