Paulo Emílio de Vilhena

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)