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.