Research
My research can broadly be seen as focusing on the development of rigorous techniques and tools that enable the specification, design and development of robust and reliable software systems through language-based techniques such as typing systems, with an emphasis on the theoretical foundations of concurrent and distributed programming and their applications in the design and analysis of modern software. Furthermore, I am committed to translating these theoretical foundations into practical frameworks and tools that enhance the design and analysis of modern software.
To this end, a significant part of my research efforts over the years has focused on the development of rich typing disciplines, able to certify various degrees of program correctness at compilation time, before any code is executed. While the majority of my research has been devoted to type systems and verification techniques for message-passing concurrent programs, I have also developed such frameworks and tools for other settings such as meta programming, generic programming and program synthesis.
In essence, my research is an ongoing attempt at answering the question: How can type theory help us to produce better, more robust systems?
Types for Channel-based Concurrency
Session types are a collection of typing disciplines for message-passing concurrency that are able to statically ensure behavioral correctness properties such as protocol fidelity and deadlock-freedom of concurrent programs. A significant part of my work in this space has focused on developing new theoretical underpinnings for session types based on a propositions-as-types correspondence with linear logic, providing a unified framework for the development of a range of advanced session-typing systems that are able to ensure stronger correctness properties of concurrent message-passing programs and are amenable to integration into programming languages. For instance, I have developed a system of dependent session types (which won the 10-year Test of Time award at the Symposium on the Principles and Practice of Declarative Programming) that can statically verify arbitrary properties of data exchanged in communication, integrated with a form of proof certificates that can be exchanged via communication and mechanically checked in the style of proof-carrying code. The framework also integrates modular notions of various forms of trust, which combine with proof certificates to validate the desired properties even in distributed settings, where agents may be controlled by different parties. I have also studied how to generalize these ideas to the verification of arbitrary correctness properties of session-typed programs through a combination of dependent types, dependent session types and advanced forms of type-level computation.
Recently, I have researched a fine-grained analysis of session interaction as provided by the linear logic typing disciplines to introduce the SAM, an abstract machine for mechanically executing session-typed processes. The SAM is able to accomodate sequential with concurrent session behaviors, such that sequential parts of session-based programs can be efficiently executed by deterministic sequential execution, free of concurrent synchronisation mechanisms.
Going beyond the foundations of channel-based concurrency, I have also explored behavioral type-based verification techniques for concurrency in Go.
Type-safe Generic (Meta-)Programming
Software development practices increasingly rely on many forms of automation, often based on tools that generate code from various types of (often imprecise) specifications, leveraging the reflection and meta-programming facilities that modern programming languages provide. Unfortunately, the standard meta-programming idioms of modern programming languages aggressively challenge the safety guarantees provided by static typing (if such exist in the language at all), which becomes especially problematic given that meta-programs are notoriously hard to test for correctness. To address this issue I have contributed to the development of a notion of refinement kind, a typing and kinding discipline that cleanly supports static type checking of type-level reflection, parametric and ad-hoc polymorphism, which can all be combined to implement sophisticated yet type-safe meta-programming idioms.
Crucially, types in our language may be reflectively manipulated as first-class (abstract-syntax) labelled trees, both statically and at runtime. Moreover, the deduction of relevant structural properties of such tree representations of types is amenable to automation using off-the-shelf SMT solvers. Remarkably, even if types in our system can essentially be manipulated by type-level functions and operators as abstract-syntax trees, our system statically ensures the sound inhabitation of the outcomes of type-level computations by the associated program-level terms, enforcing type safety, and allowing our language to express challenging reflection idioms in a type-safe way.
Verification of Message-Passing Programs
I have used Rust’s advanced type system to implement shared session typing as an idiomatic embedded DSL (eDSL) in Rust dubbed Ferrite, such that protocol violations are in the eDSL are detected by the Rust type-checker (i.e., at compile time). We have used Ferrite to refactor part of Firefox’s Servo engine and used the type-based protocol analysis to uncover a protocol violation in the Servo implementation. The work received a distinguished paper award at ECOOP’22.
Type-based Synthesis
Program synthesis consists of a range of techniques that aim to automatically generate code given a high-level specification of its intended functionality. Program synthesis can thus be used to alleviate many of the challenges of modern programming, provided that users can adequately express their intent to the synthesizer in the form of an adequate specification. Type-based synthesis consists of using rich \emph{types} as specifications for synthesis, often relying on techniques based on proof search via the connections between proof theory and type theory. In this space, I have worked on synthesis of functional programs based on linear types, leveraging proof search techniques for linear logic. The resulting work is able to efficiently synthesize functional programs for a Haskell-like language featuring first-class polymorphism, algebraic data types, recursive functions and linearity. This allows us to, e.g., automatically synthesize the code for a mutable array interface.
Logical Foundations of Hardware Description Languages
Digital circuits describe computations whose functional correctness depends on various timings properties of the circuit components. As an example, an inverter will typically have some propagation delay (a maximum time interval between the start of its input and the start of its output signal) and a contamination delay (the minimum time between the end of the input until the end of the output). Thus, to specify and reason compositionally about the functional correctness of such digital circuits one needs to reason about the time intervals in which signals that act as input and output to circuit components are, or are not, available.
To this end, I have investigated (together with a current PhD student enrolled in the CMU Portugal dual-degree program in CS) a notion of constructive or intuitionistic metric temporal logic, where propositions can refer to continuous time intervals and where every proof corresponds to a temporal computation (in the sense that all proofs respect the flow of time). Using this logic, we can model the timed interactive behaviour of digital components such as NOT and NAND gates. These may then be assembled into so-called combinational circuits, and their non-trivial temporal correctness can be checked using our logic.
Generic Programming in Go
The Go programming language infamously lacked generic programming features. After significant outcry from Go developers, generics were added to the language in version 1.18 (in 2022, 15 years after the language’s first release). I was one of the researchers involved in the development of Featherweight Generic Go. This collaboration between academics and Google’s Go language team resulted in the development of two minimal models of (non-generic) Go and generic Go, and on the formalization of a translation of generic to non-generic Go based on monomorphisation (akin to template specialization in C++), effectively serving as a way to \emph{compile} generic Go. The resulting work served as the formal basis for the addition of generics to Go, released in version 1.18 and expanded upon in subsequent versions. The compilation strategy used by Go generics to this day is based on the monomorphisation strategy of our work.