I’m interested in building strong theoretical foundations for pragmatic PL features. During my PhD in Martin Odersky’s lab I focused on the theory of Capture Tracking for Scala. Also, I worked on SuperF, a type inference algorithm for System F and added subtyping reconstruction, a novel OO take on GADTs, to the Scala compiler.
Developing some very desireable PL features, like type inference, requires taking on additional complexity to improve the life of the language’s users. After a certain point, the only way to implement such features without completely losing track of what’s going on involves developing and studying appropriate formal foundations.
I’m also interested in:
If you see how all three are connected, let’s chat :)
Tracking the Capture of capabilities in types.