Programming Languages; Program Verification; Software Engineering

Currently supervising 3 PhD students:
- Elizabeth Labrada. To be defended in 2021/early 2022.
- Stefan Malewski. Started 2020.
- Bruno García Agapito da Veiga. Started 2021.

Currently supervising 1 MSc student:
- Damian Arquez [co-advised with Matías Toro]. To be defended in 2021.

Currently closely involved in the co-supervision of PhD students abroad:
- Joseph Eremondi, University of British Columbia, Canada, with Prof. Ronald Garcia
- Meven Bertrand, Inria Rennes, with Dr. Nicolas Tabareau
- Jenna Wise, Carnegie Mellon University, USA, with Jonathan Aldrich

Graduated 9 PhD students:
- Raimil Cruz: Type Abstraction and Faceted Types for Declassification. Defended 15/01/2020.
- Matías Toro: Abstracting Gradual Typing: Metatheory and Applications. Defended 05/07/2019.
- Oscar Callaú: Empirically-Driven Design and Implementation of Gradualtalk. [co-advised with Romain Robbes]. Defended 27/01/2015.
- Esteban Allende: Improving the Efficiency and Reliability of Gradual Typing [co-advised with Johan Fabry]. Defended 08/01/2015.
- Rodolfo Toledo: Modular and Secure Access Control with Aspects. Defended 13/05/2014.
- Ismael Figueroa: Effective Aspects: A Typed Monadic Model to Control and Reason About Aspect Interference [co-advised with Nicolas Tabareau]. Defended 22/04/2014.
- Christophe Scholliers: Ambient Contracts (Vrije Universiteit Brussel) [co-advised with Wolfgang De Meuter]. Defended 07/02/2013.
- Paul Leger: Opening Up Trace-Based Mechanisms. Defended 05/10/2012.
- Guillaume Pothier: Towards Practical Omniscient Debugging. Defended 13/06/2011.

Graduated 9 MSc students:
- Hans Fehrmann: A Reasonably Exceptional Type Theory [co-advised with Nicolas Tabareau]. Defended 29/12/2020.
- Fabian Mosso: Countable Polymorphic May-Must Effects [co-advised with Matías Toro]. Defended 12/06/2020.
- Nicolás Lehmann: Gradual Refinement Types. Defended 9/3/2017.
- Johannes Bader: Gradual Program Verification with Implicit Dynamic Frames (Karlsruhe Institute of Technology) [co-advised with Jonathan Aldrich (CMU) and Gregor Snelting (KIT)]. Defended 4/10/2016.
- Gustavo Soto: Modular Composition of Session Types. Defended 1/12/2015.
- Matías Toro: Customizable Gradual Effects for Scala. Defended 18/05/2015.
- Felipe Bañados: Gradual Typing for Generic Type-and-Effect Systems [co-advised with Ron Garcia]. Defended 08/08/2014.
- Milton Inostroza: Safe and Practical Decoupling of Aspects with Join Point Interfaces [co-advised with Eric Bodden]. Defended 12/04/2013.
- Victor Ramiro: An Open Proximity Model for Service Discovery in Pervasive Computing. Defended 2009.

Awards from industrial partners:
- In 2015 and 2016, I was awarded a Google Faculty Research Award, for working on the principles of gradual security typing for the Web, together with my PhD student Raimil Cruz.
- With Jonathan Aldrich's group at Carnegie Mellon University, I was awarded a Facebook Research Testing and Verification Award in 2018, for developing the principles and applications of gradual verification.
Both awards had high media coverage globally, giving visibility to the areas of gradual typing and incremental program verification.