In this seminar, I will discuss how to formalize normalization-by-evaluation of dependently typed theories in Agda. We will mainly focus on two systems: MLTT (we will discuss what we mean by MLTT in the talk) with a cumulative and non-cumulative universe and show the soundness of completeness of NbE using logical relations (closely related to Chapter 6 of ATTAPL). This is a joint work with Jason Hu from McGill.