Thesis

I describe Viaduct, a compiler that transforms high-level programs into secure, efficient distributed realizations that use cryptography. I develop a modular security proof for Viaduct that abstracts away from the details of cryptographic mechanisms.

Prior work has established the logical connection between linear sequent calculus and session-typed message-passing concurrent computation. In this thesis, I extend the basic type system with intersection and union types in order to express multiple behavioral properties of processes in a single type.