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.