I studied programming languages in Martin Odersky's group at EPFL and worked on Scala, specifically pattern matching. dblp

After I joined Google, I continued my study formal logic, type theory and category theory for programming and specifying program behavior.

Here are some artifacts:

Pattern Matching

Pattern matching and ML-style algebraic data types are now part of rust, Java and python3.

Constrained Polymorphism

During an internship at Microsoft Research in Cambridge, I got to apply some Scala techniques to C#. The results are described here:

Variance annotations made it into C# 4.0 later.

Symbolic Execution

At Google (2010?), I got a 20% intern sponsorship to host Stefan Bucur on a project related to Cloud9. We tried symbolic execution as an alternative to fuzzing to look for vulnerabilities in Chrome. This did not work well at the time, though we learned a lot (this was before Google had a consistent cloud offering). Stefan joined Google later and is working in security.

Systems, Languages, Types, Logic

There are many kinds of scientific and theoretical knowledge that have deep practical applications.

This is especially true in the context of distributed systems. I am preparing a few artifacts around these topics that I will publish here.