Interaction Trees and Formal Specifications

Interaction Trees are a recently developed form of denotational semantics for effectful programsthat is executable and compositional. This dissertation uses Interaction Trees to develop reusable, language-independent tools for different classes of specifications. First, it demonstrates how to apply the Dijkstra monads (Swamy et al., 2013; Maillard et al., 2019) approach to Interaction Trees. Second, it demonstrates how to analyze the information flow properties of Interaction Trees, enabling security analysis for any programs with Interaction Tree denotations. Finally, it presents the Interaction Tree Specification framework, a program logic for Interaction Trees that enables efficient, syntactic automated proofs of properties of Interaction Trees.