## Advanced

#### Normalization by Evaluation

A normalization by evaluation algorithm for an intrinsically typed simply-typed lambda calculus.

#### Weak Normalization

A proof of weak head normalization for the simply typed lambda calculus using logical relations.