Algebraically Closed Fields in Isabelle/HOL. - Paulo Emílio de Vilhena; Lawrence C. Paulson (IJCAR (2), 2020)

Spy game: verifying a local generic solver in Iris. - Paulo Emílio de Vilhena; François Pottier; Jacques-Henri Jourdan (Proc. ACM Program. Lang., 2020)

Verifying a Minimalist Reverse-Mode AD Library. - Paulo Emílio de Vilhena; François Pottier (CoRR, 2021)

A separation logic for effect handlers. - Paulo Emílio de Vilhena; François Pottier (Proc. ACM Program. Lang., 2021)

A Type System for Effect Handlers and Dynamic Labels. - Paulo Emílio de Vilhena; François Pottier (ESOP, 2023)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library. - Paulo Emílio de Vilhena; François Pottier (Log. Methods Comput. Sci., 2023)

Extending the C/C++ Model with Inline Assembly. - Paulo Emílio de Vilhena; Ori Lahav 001; Viktor Vafeiadis; Azalea Raad (CoRR, 2024)

Extending the C/C++ Memory Model with Inline Assembly. - Paulo Emílio de Vilhena; Ori Lahav 001; Viktor Vafeiadis; Azalea Raad (Proc. ACM Program. Lang., 2024)