*e-mail:
f...@andrew.cmu.edu
*

I am currently a second year Ph.D. student in the Philosophy Department at Carnegie Mellon University. My advisor is Jeremy Avigad and I am enrolled in the Pure and Applied Logic program.

I previously studied at the Utrecht University in the Netherlands
where I received a B.Sc. in Mathematics, a B.Sc. in Physics and a M.Sc. in Mathematics.
My master thesis is *Explicit convertibility proofs in Pure Type Systems*
supervised by Freek Wiedijk at the Radboud University Nijmegen.

I'm currently working on interactive theorem proving, working on the standard library for a new proof assistant Lean which is developed by Leo de Moura at Microsoft Research. I'm also working on the formalization of Homotopy Type Theory in Lean.

I'm interested in mathematical logic in general, and particularly in type theory, category theory, set theory and model theory.

- Fall 2014: TA for Formal Logic (80-310/80-610) with Steve Awodey.

- Spring 2012: TA for Discrete Mathematics with Han Hoogeveen.
- Fall 2011: TA for Foundations of Mathematics with Jaap van Oosten.

- Cody Roux and Floris van Doorn.
*The Structural Theory of Pure Type Systems*, in Types and Lambda Calculi and Applications, 2014. (slides) - Floris van Doorn, Herman Geuvers, Freek Wiedijk,
*Explicit Convertibility Proofs in Pure Type Systems*, Proceedings of LFMTP 2013, 2013. (Coq formalization)