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.