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
-
Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library (LMCS 2023)
Paulo Emílio de Vilhena and François Pottier
(pdf) (arxiv) -
A Type System for Effect Handlers and Dynamic Labels (ESOP 2023)
Paulo Emílio de Vilhena and François Pottier
Nominated to one of the best paper awards
(pdf) (doi) (slides) -
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)
Recipient of the thesis award from the GDR GPL
(pdf) (slides)