Former Student
I'm working on the formalization of metatheoretic proofs of type theories. My bachelor's thesis was supervised by Chad E Brown and considered Confluence and Termination of CC with Sigma types, using the reducibility candidates technique. In summer 2014 I considered the Termination framework of Bernadet and Lengrand (using non-idempotent intersection types) and worked on a formalization in Coq.