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.
A normalization by evaluation algorithm for an intrinsically typed simply-typed lambda calculus.
A proof of weak head normalization for the simply typed lambda calculus using logical relations.