Pierre-Evariste Dagand

Binding

I’m a CNRS researcher at LIP6, where I am a member of the team Whisper. My work revolves around making safer Systems software through domain-specific languages (DSLs) and formal verification (and, in particular, using and abusing of interactive theorem provers).

Prior to joining LIP6, I was a postdoctoral researcher in the Gallium team at INRIA Paris. There, I have worked with François Pottier and Didier Rémy. This involved some Mezzo, and some ornamentation.

And before all that, I was Conor McBride’s PhD student. During my PhD, I’ve worked on the theory behind the intensional fragment of Epigram. I’ve studied some universes of data-types and the possibilities offered by such an approach. If Epigram were to be (eventually) implemented, it might contain the cool stuff I’ve modelled with polynomial functors.