Paulo Emílio de Vilhena

Paulo's webpage

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

  • A Separation Logic for Effect Handlers (POPL 2021)
    Paulo Emílio de Vilhena and François Pottier
    (pdf) (doi) (talk)

  • Algebraically Closed Fields in Isabelle/HOL (IJCAR 2020)
    Paulo Emílio de Vilhena and Lawrence C. Paulson
    (pdf) (doi) (talk)

  • Spy Game: Verifying a Local Generic Solver in Iris (POPL 2020)
    Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan
    (pdf) (doi) (talk)