This semester, I took a course on the science of cybersecurity, targeted toward an audience with some programming languages background.

A classmate and I had a semester long research project on “erasable” code contracts. More details are below.

This was a valuable experience, giving me an opportunity to work on two things that I hadn’t done before:

1. Proof-based research
2. Basic proofs of a calculus. While type soundness proofs and their associated lemmas are core to many calculi, many introductory programming language courses, including the one that I took, skip the details of the proofs.

Here’s the abstract:

Contract programming is a design approach that allows programmers to design formal specifications for software, known as “contracts”. These contracts, executed at runtime, allow programmers to make assertions about the behavior of their software and ensure program correctness. In a language with side-effects, however, it is possible for these contracts to modify memory and consequently change the behavior of the program. While contracts provide the specifications, these specifications clearly should not change the behavior of the program that they enforce. Instead, if the contracts were removed (“erased”), then the behavior of the program should be the same as if the contracts remained. This notion is captured by the idea of erasability. We present a calculus for erasable contracts, establish properties such as type soundness, and prove a formal definition of erasability for the language.

Download the PDF or view it below. Note that it’s missing some of the grittier nuances of the eta-reductions.