About | Robbert Krebbers
Patoline
I am a researcher in computer science, currently working as a postdoctoral researcher at the Max Planck Institute for Software Systems in Saarbrücken, in Derek Dreyer 's group. Although my interests are diverse, my main area of expertise is the application of semantic techniques to programming languages and proof assistants. I also make a point of backing my theoretical work with a substantial amount of implementation, for which I developed specific tools and libraries in OCaml .
Between September 2017 and December 2018, I was a postdoctoral researcher at Inria in the Deducteam project, hosted by the LSV at ENS Cachan (now ENS Paris-Saclay). During that time, I proposed a new implementation of the Dedukti logical framework called Lambdapi , which enables the development of mathematical proofs in the system, while the original Dedukti was only usable as the target of translations.
Between October 2014 and August 2017, I was a PhD student at the LAMA (LAboratoire de MAthématiques), in Chambéry (in the French Alps). During that time, I mainly worked with Christophe Raffalli and Pierre Hyvernat , although my official advisor was Karim Nour . In my thesis work, I designed the theoretical foundation of (and implemented) the PML₂ language, which mixes programming and program certification in a uniform (ML-like) setting.
About | Robbert Krebbers
Patoline