Weak βη-normalization and normalization by evaluation for System F

Abstract. A general version of the fundamental theorem for System F is presented which can be instantiated to obtain proofs of weak β- and βη-normalization and normalization by evaluation. 1 Introduction and Related Work Dependently typed lambda-calculi have been successfully used as proof languages in the proof assistants Agda [Nor07], Coq [INR07], LEGO [Pol94], and NuPrl [Ct86]. Since types may depend on values in these type theories, checking equality of types, which is crucial for type and, thus, proof checking, is non-trivial for thes