We prove the end-to-end correctness of a compiler that synthesizes cryptographic protocols from high-level programs. The proof is based on the Universal Composability framework.

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.

We present Viaduct, a compiler that transforms high-level programs into efficient distributed realizations that use cryptography to preserve security.

We extend the deep logical connection between linear sequent calculus and session-typed concurrency with intersection and union types to express multiple behavioral properties of processes.

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.