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

I am a Marie Sklodowska-Curie Fellow working at at NOVA-LINCS, Universidade Nova de Lisboa.


Since June 2020, I am a Marie Sklodowska-Curie Fellow working at at NOVA-LINCS, Universidade Nova de Lisboa. My research project, entitled Cameleer, aims at developing tools and techniques for the deductive verification of OCaml programs. More details can be found in my proposal. More information about this project can be found here.

From 2015 to 2018 I was a PhD candidate at LRI, Université Paris-Saclay. My supervisor was Jean-Christophe Filliâtre and I was conducting my research in the VALS team. I was 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 was 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

I gather in this section a selected set of documents and links about the activity of program verification. I also publish examples that I had fun proving myself.

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:

We can find me on GitHub under the name mariojppereira.


Since 2020 I am teaching assistant at FCT/Universidade Nova de Lisboa. The following courses material are mainly given in Portuguese:

Theory of Computation lecturer: António Ravara 2019-2020
Analysis and Design of Algorithms lecturer: Margarida Mamede 2020-2021

From 2016 to 2018 I 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)