Rigorous reasoning about implementations of software systems requires a detailed math- ematical model of the behavior of the programming language. However, real-world pro- gramming languages are rich in features, and their mathematical models are complex and unfeasible to reason about directly. We need powerful mathematical machinery to alle- viate this complexity and make it viable to reason formally about programs implemented in real-world programming languages. This Ph.D. dissertation is a collection of five papers that develop and apply higher- order separation logics to tame the complexity of mathematical models for rich program- ming languages in the context of distributed systems, a type system for information-flow control, and contextual equivalence of probabilistic programs. The first part of the dissertation develops a higher-order distributed separation logic that allows us to reason modularly about network-connected distributed applications that run on multiple machines while communicating over an unreliable network. We argue through several case studies that the logic is a solid foundation that makes verifying a range of distributed systems and protocols feasible. We also show how distributed systems can be verified and specified by establishing simulation relations with abstract models. The second part of the dissertation is concerned with an expressive static information- flow control type system that guarantees that a well-typed program’s public behavior is independent of its secret inputs. We develop a semantic model of the type system in a higher-order separation logic that allows us to prove that the type system is sound. Using the model, we also show how to compositionally integrate syntactically ill-typed—but semantically secure—components with well-typed programs. The third and final part of the dissertation develops a relational higher-order sepa- ration logic for reasoning about contextual equivalence of probabilistic programs imple- mented in an expressive programming language with higher-order local state and poly- morphism. We develop a proof method for relating asynchronous probabilistic samplings in a program logic and demonstrate the approach’s usefulness with several case studies
2023-03
2026-06-23