DCC. Implementation of Defunctionalized Calculus of Constructions (Master thesis)
5Defun. PartIII dissertation: defunctionalization for dependently typed languages
4ShallowStack. Dependently typed stack machine language prototype in Agda
4HereditarySubstitution. An formalization of hereditary substitution for STLC
1