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.

A short adventure into the depths of optional and/or keyword functions in Racket.

Several old questions from the Typed Racket mailing list have new and simple answers under a “transient” Typed Racket.

What type-directed optimizations does Typed Racket perform and do any require full types?

On November 11th 2019, the PRL had a private offsite meeting at the More Than Words bookstore in downtown Boston. For future offsite organizers, this post records what happened and how.

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.

This post explains how to get started using Scribble to write a research paper.

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