Hi, I am a member of the Graduate School of Computer Science and a PhD student at the Programming Systems Lab here in Saarbrücken.
I am currently studying the various ways syntax with binders can be handled in a proof assistant. I am using System F as an object logic that has sufficiently interesting binding mechanisms and compare and contrast an equivalence proof done with de Bruijn syntax in Coq with a HOAS approach in Abella and Beluga.
Prior to my present line of work I focused on the construction of models for type theories. In particular I worked with set-theoretic models for Luo's ECC.I am mainly interested in Computational Logic, Type Systems, Syntax with Binders, Functional Programming and Programming Language Semantics.
I received my BA (Hons) in Computer Science from the University of Cambridge in 2010 and a M.Sc. from Saarland University in 2013.