I’m a PhD student under the supervision of François Pottier.
We are interested in devising methods for reasoning with rigour about computer programs:
how to write a precise documentation of their behaviour and how to prove that such a specification is met.
In particular, we study programs that both manipulate the heap and alter the control flow through effect handlers, a new and exciting programming language construct.
Verifying a Minimalist Reverse-Mode AD Library (Submitted to LMCS)
Paulo Emílio de Vilhena and François Pottier