Student Mentoring and Advising
Current Students
- Luíz de Sá (PhD), working on types for hardware design (co-advised with Frank Pfenning).
- Joana Faria (MSc), working on compiler optimizations for session-typed languages.
- Gonçalo Lourenço (MSc), working on implementation of session typing systems that go beyond linearity.
- Hugo Moreira (MSc), working on implementation of modularity and generic programming features in a session-typed language.
- Rodrigo Mesquita (MSc), working on type-preserving optimizations in GHC’s (linear) Core.
Past Students
- João Geraldo (MSc), Making Session Types Go, 2022.
- David Costa (MSc), Session Kotlin, 2022.
- João Pereira (MSc), Featherweight Generic Go with Untyped Constants, Structural Type Definitions and Type Inference, 2022.
- Sara Almeida (MSc, co-advised with João Seco), Type-driven Synthesis of Evolving Data Models, 2021.
- Lenino Dias (MSc, co-advised with Vasco Silva from OutSystems), OutSystems Logic Previewer, 2021.
- Rodrigo Mesquita (Undergraduate Research), Type-based Synthesis of Linear Functional Programs, 2021.
- Gonçalo Almeida (MSc Industry Project), 2020.
- Gabriel Marcondes (MSc Industry Project), 2019.
- Filipe Farinha (MSc Industry Project), 2019.
Links to student reports and theses can be found here.
Applying to Join the Group
If you had a look at my Research and/or Publications page and found the kind of research I do interesting, feel free to drop me an email. I am almost always interested in eager new MSc students and definitely always interested in PhD students.
Prospective MSc Students
In the CS department at NOVA SST, advisors usually publish a list of MSc thesis topics at the beginning of each semester, so be on the look out for my topics if you are interested.The unwritten protocol is that students should apply to the topic using CLIP, but also get in touch with the person who proposed the topic, signaling their interest (and why they are interested!), so that a meeting can be set-up to determine if the topic is a right fit for the student's interests and academic expertise.
Important Note: If you are keen on working with me, don't wait for the topics to be posted online, get in touch! I am more than happy to craft a thesis topic aligned around our shared interests.
Prospective PhD Students
If are interested in doing a PhD with me, drop me an email explaining your topics of interest and why you are interested in doing a PhD. Formally, you will have to apply to the CS PhD program in my department, but I am more than happy to guide you through the process. I also have various research collaborations with universities in the UK and with Carnegie Mellon University, with which co-supervisions are often possible. If this is something you'd be interested in, I strongly urge you to contact me ASAP, since the timings and requirements to apply for these PhD programs can be very different from those at NOVA.Mentoring
Regardless of how far into your academic career you are, if you are curious about Academia, Computer Science, Programming Languages or what research in CS means, feel free to get in touch!Student Theses and Project Reports
- Synthesis of Linear Functional Programs[Code]Undergraduate Research Project, School of Science and Technology, NOVA University of Lisbon, 2021
- Designing and Implementing a Compiled Programming Language with Session-Typed Concurrency[Abstract, PDF]MSc thesis preparation, School of Science and Technology, NOVA University of Lisbon, 2020
Modern software practices fundamentally require programmers to take a concurrency- first approach to program development and design, due to heterogeneous resource inter- action, strong availability requirements and explosion in ubiquitousness of multi-core architectures. With the shift towards pervasive concurrent programming, programming languages have also evolved in terms of concurrency related features, providing users with high-level concurrency primitives such as green-threads, thread-pools, mailboxes, channels, and mechanisms for asynchronous execution (e.g. async-await, events, futures), that enable programmers to express higher-level designs in a more natural way. However, even languages with strong type-safety guarantees are not able to provide any but the most basic static correctness guarantees in these concurrent settings, being only able to ensure type safety but failing to guarantee deadlock-freedom or protocol fidelity.
In this work, we leverage a family of type systems for concurrency dubbed session types, which can be used to statically ensure communication safety and protocol fidelity, in order to implement a concurrent programming language that provides high-level concurrency features such as communication channels, process spawning and channel passing, and also strong-safety guarantees such as protocol fidelity and deadlock-freedom. Concretely, we will develop a type checker, interpreter and compiler for a session-typed functional language with the features mentioned above, whose design is inspired by previous work. The type checker will employ state-of-the-art bidirectional type checking techniques, and the compiler will target a realistic backend (such as the JVM or LLVM), potentially making use of the logical properties of the type system to optimize execution.
- Type-driven Synthesis of Evolving Data Models and APIs[Abstract, PDF]MSc thesis preparation, School of Science and Technology, NOVA University of Lisbon, 2020
Modern software practices fundamentally require programmers to take a concurrency- first approach to program development and design, due to heterogeneous resource inter- action, strong availability requirements and explosion in ubiquitousness of multi-core architectures. With the shift towards pervasive concurrent programming, programming languages have also evolved in terms of concurrency related features, providing users with high-level concurrency primitives such as green-threads, thread-pools, mailboxes, channels, and mechanisms for asynchronous execution (e.g. async-await, events, futures), that enable programmers to express higher-level designs in a more natural way. However, even languages with strong type-safety guarantees are not able to provide any but the most basic static correctness guarantees in these concurrent settings, being only able to ensure type safety but failing to guarantee deadlock-freedom or protocol fidelity.
In this work, we leverage a family of type systems for concurrency dubbed session types, which can be used to statically ensure communication safety and protocol fidelity, in order to implement a concurrent programming language that provides high-level concurrency features such as communication channels, process spawning and channel passing, and also strong-safety guarantees such as protocol fidelity and deadlock-freedom. Concretely, we will develop a type checker, interpreter and compiler for a session-typed functional language with the features mentioned above, whose design is inspired by previous work. The type checker will employ state-of-the-art bidirectional type checking techniques, and the compiler will target a realistic backend (such as the JVM or LLVM), potentially making use of the logical properties of the type system to optimize execution.