Research
My research broadly focuses on the application of language-based techniques to the development of more robust systems, with an (non-exclusive) emphasis on concurrent and distributed settings. In these realms, I develop and apply techniques grounded on (substructural) type theory, such as those based on Linear Logic and Session Types. I am also interested in using advanced type and logic-based techniques to verify and reason about programs in real languages such as Go, Rust and Haskell. 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
To explore this question for concurrent programs, my main body of work lies in the study and development of the logical foundations of session-based concurrency, arising from the propositions-as-types interpretation of linear logic. 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
Automated code generation, domain specific languages, and meta-programming are increasingly becoming productivity drivers for the software industry, while also making programming more accessible to non-experts, and, more generally, increasing the level of abstraction expressible in languages and tools for program construction.
Unfortunately, meta-programming constructs and idioms aggressively challenge the safety guarantees of static typing, which becomes especially problematic given that meta-programs are notoriously hard to test for correctness. My work in this space aims to try to bring such idioms back into the realm of type-safety, by developing sufficiently advanced, yet usable, typing systems.