Paulo Emílio de Vilhena

Profile Picture

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

  • Extending the C/C++ Memory Model with Inline Assembly
    Object-Oriented Programming, Systems, Languages & Applications (OOPSLA), October 2024
    Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, and Azalea Raad
    [ pdf | doi ]
  • 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 ]

PhD Thesis