I am a postdoctoral researcher at Imperial College London working under the supervision of Azalea Raad on the theoretical foundations of persistent memory. During my thesis, supervised by François Pottier, I devised extensions of Separation Logic with support for effect handlers.
Publications
-
A Type System for Effect Handlers and Dynamic Labels (ESOP 2023)
Paulo Emílio de Vilhena and François Pottier
(pdf) -
Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library (Submitted to LMCS)
Paulo Emílio de Vilhena and François Pottier
(pdf) -
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) -
Proof of Programs with Effect Handlers (PhD Thesis – 2022)
(pdf)