Hello and welcome to my small corner in the web! :D
I am an Assistant Professor at NOVA School of Science and Technology. I am also an Integrated Member of NOVA LINCS.
Research
From June 2020 to May 2022, I was a Marie Sklodowska-Curie Fellow working at at NOVA-LINCS, NOVA University of Lisbon. My research project, entitled Cameleer, main goal was 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:- (in Portuguese) An introductory lesson to program verification and the Why3 tool, by Simão Melo de Sousa.
- A paper by Jean-Christophe Filliâtre, surveying the area of deductive software verification with an emphasis on tools. Excelent reading for beginners and those seeking a large view of nowadays program verification activity.
My own "proof pearls"
Programming
I really love computer programming, especially functional programming. I am a big fan of the OCaml language.
I am contributing to the following software:
- Cameleer, a deductive verification tool for OCaml
- Why3, a software verification framework
- OCamlGraph, a graph library for OCaml
- VOCaL, the Verified OCaml Library
We can find me on GitHub under the name mariojppereira.
Teaching
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) |