About Me

I am an Assistant Professor at the HKUST CSE department since February 2021. I am looking for students to join my research group! Please contact me (first-name dot last-name at gmail.com) if you’d like to work on something related to programming languages, type systems, or compiler optimization.

I obtained my PhD in 2020 at EPFL, in the Data Analysis Theory and Applications Laboratory (DATA), where I created the Squid type-safe metaprogramming library for Scala.

My interests include: functional programming; dependent types; effect systems; compilers; metaprogramming; high-level program optimization; embedded domain-specific languages; query languages; database systems; verification; video games design and development; physics engines…

Programming Languages

For me, programming languages are more than “just tools” to tell computers what to do; they are, equally importantly, vectors for expressing thoughts in a rigorous way, and for communicating these thoughts to other humans.

I would venture to say that good programming is not unlike good writing, and even sometimes resembles poetry. There is something beautiful in a well-typed program clicking together, dancing around the landmines of runtime errors with the strong confidence conferred by its type system. And there is something unique in the humbling experience of having a compiler tell us, rightly, that we are wrong, and that we need to revise our mental model of a problem.

Of course, compilers are often wrong themselves, so it is one of my personal missions to make compilers less often wrong, and to make them more understandable and less frustrating when, unavoidably, they are.

Abstraction Without Regret

I am not interested in abstraction for its own sake — my end goal has always been to build useful, practical software with a focus on correctness, maintainability, and performance.

High-level and especially functional programming languages offer good solutions to twe first two of these goals, but these languages typically incur a lot of runtime overhead, defeating the third one. Moreover, functional languages usually provide little in the way of controlling that overhead, so the only option, when performance is critical, is often to rewrite our programs in terms of more error-prone, lower-level abstractions.

As part of my research, I have developed new ways of regaining some control on the performance of functional programs, without giving up on high-level abstractions. I have worked on developing novel metaprogramming approaches extending the multi-stage programming discipline. As part of that effort, I am developing a staged database compiler which integrates seamlessly into Scala applications, removing the application/database impedance mismatch, while also leveraging traditional performance-oriented database implementation strategies.

I have recently been working on a new graph-based intermediate representation for optimizing functional languages, which can be used to partially evaluate programs without having to rely on aggressive inlining and the resulting excessive code duplication. One of the goals of this technique is to provide some hard guarantees on the removal of abstractions from user programs, so that one can develop abstract, modular code “without fear” and “without regret.”

The name of the blog, Well-Typed Reflections, is a pun on the double meaning of reflection, which is both the act of “engaging in serious thought or consideration,” and a metaprogramming technique. Since a central topic of my PhD has been to use type systems for making metaprogramming safer, I naturally prefer the latter activity to be well typed. But as a philosophical stance, I think we should strive to make our everyday reflections “well typed” too, applying the same kind of rigor and clarity we use in formal methods to philosophy, politics, and societal issues.