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

I am a PhD student at LRI, Université Paris-Sud. 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. In the scope of my PhD, I'm studying ways to extend Why3 to support higher-order (effectful) programming.

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 Mario 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 Simao Melo de Sousa.

Program proofs


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