Old Post

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.

New post

We will turn our focus to the non-cunmulative system this time, but now we have some more results (and better notations!). I will also share some lessons and tricks learned in mechanization. As this talks is supposed to be a problem session, I will try to provide some contents about future work.