This repository contains two proofs for the normalization of the simply-typed lambda calculus using the language Agda.
-
Tait: Proof following the logical relations style as originally formulated by Tait.
-
NbE: Proof following the normalization-by-evaluation algorithm