Non-nullable Reference Types for Scala

We’re trying to get rid of null in Scala. Statements like val x: String = null will no longer typecheck (and we’ll reduce those pesky NPEs). Here’s the design doc and code, based on Dotty.


Program Disequivalence for MIPS

When are two MIPS programs (dis)equivalent, and how can we tell? For this project, I used concolic execution to verify when two MIPS programs are disequivalent. Here’s the resulting tool, Tamarin, and tech report.

Algorithmic Typing for DOT

The Dependent Object Types (DOT) calculus is a formalizaton of a (tiny) subset of Scala. The typing rules for DOT have a declarative, as opposed to algorithmic, style, so we can’t implement them in a typechecker. In this project, I proposed an algorithmic (and decidable) version of the DOT typing rules that can type a subset of the calculus. Details in the paper.