I successfully defended my Ph.D. dissertation. You can find the document, a talk recording, and much more here:

• http://ccs.neu.edu/home/types/publications/publications.html#g-dissertation-2020

To the PRL: thanks for a wonderful 6.5 years.

Syntactic type soundness is too weak to tell apart different ways of running a program that mixes typed and untyped code. Complete monitoring is a stronger property that captures a meaningful distinction — a language satisfies complete monitoring iff it checks all interactions between typed and untyped code.

Forgetful and heedful are two methods for space-efficient contracts developed by Michael Greenberg in 2014. These methods were born in the shadow of a third method, eidetic, with stronger theoretic properties. Since then, however, the forgetful method has been re-invented at least twice. Both deserve a second look.

The transient approach to migratory typing (circa 2014) is similar to type erasure in Java (circa 2004) in a few interesting ways.

The literature on mixed-typed languages presents (at least) three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. Recently, we have been sorting them out.

This post explains the sampling method introduced in the paper On the Cost of Type-Tag Soundness