Hello and welcome to my small corner in the web! :D

I am a PhD candidate at LRI, Université Paris-Saclay. My supervisor is Jean-Christophe Filliâtre and I am conducting my research in the VALS team.


I'm doing research in Deductive Software Verification. I'm an enthusiast of the Why3 tool and more generally of the auto-active approach to program verification. The scope of my PhD work is the VOCaL project, where we build a formally verified OCaml library using Why3.

From 2012 to 2014 I was a master student at the Computer Science Department at University of Oporto. During my master thesis I studied refinement type systems, particularly Liquid Types, and intersection types. I designed and implemented a new type system combining refinement predicates and the accuracy offered by intersection types discipline, the Liquid Intersection Type system. This work is described in my master thesis and in this paper. My supervisors were Sandra Alves and Mário Florido.

From 2009 to 2012 I was an undergraduate student at the Computer Engineering Department of University of Beira Interior. As my bacherol final project, I developed a platform to specify and prove programs written in ARM Assembly language. Take a look at this paper if you got interested. My supervisor was Simão Melo de Sousa.

Program verification

Verifying programs has been a constant in my academic life. I made my first experiences around program proving (using the Why3 tool) in 2011, at the age of 20. It comes with no surprise that I am still doing verification these days and that this ended up being my PhD research area.

What is program verification?

Who better than the masters to explain this amazing subject? Let them speak:

My own "proof pearls"


I really love computer programming, especially functional programming. I am a big fan of the OCaml language.

I am contributing to the following software:


For the past three years I have served as a teaching assistant (vacataire) at École Polytechnique. The following courses material is given in French:

INF311 (Introduction to Computer Science) lecturer: François Morrain 2015-2016 (40 hours)
INF411 (Programming and Algorithms Basis) lecturer: Jean-Christophe Filliâtre 2016-2017 (32 hours)
INF441 (Advanced Programming) lecturer: Xavier Rival 2016-2017 (32 hours)
INF411 (Programming and Algorithms Basis) lecturer: Jean-Christophe Filliâtre 2017-2018 (32 hours)
INF564 (Compilers) lecturer: Jean-Christophe Filliâtre 2017-2018 (18 hours)