Paulo Emílio de Vilhena
About me
Hi, welcome to my page! I'm a postdoctoral researcher at Imperial College London, working as a member of Azalea Raad's research group Veritas.
I did my PhD at Inria Paris, in the Cambium research team, under the supervision of François Pottier. The main contribution of my thesis is the extension of Separation Logic with support for effect handlers, an advanced control-flow mechanism that was recently added to OCaml (coincidentally, in the same day as my thesis defense!).
Publications
-
Verifying an Effect-Handler-Based
Define-By-Run Reverse-Mode AD Library
Logical Methods in Computer Science (LMCS), October 2023
Paulo Emílio de Vilhena and François Pottier
[ pdf | doi | arxiv ] -
A Type System for Effect Handlers and Dynamic Labels
European Symposium on Programming (ESOP), April 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
Principles of Programming Languages (POPL), January 2021
Paulo Emílio de Vilhena and François Pottier
[ pdf | doi | talk | slides ] -
Algebraically Closed Fields in Isabelle/HOL
International Joint Conference on Automated Reasoning (IJCAR), June 2020
Paulo Emílio de Vilhena and Lawrence C. Paulson
[ pdf | doi | talk | slides ] -
Spy Game: Verifying a Local Generic Solver in Iris
Principles of Programming Languages (POPL), January 2020
Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan
[ pdf | doi | talk | slides ]