Cost-sensitive programming, verification, and semantics

Although the pure functional semantics of computer programs has been well-studied since at least the seminal work of Scott and Strachey, it has remained challenging to integrate cost structure and the ability to speak about cost-sensitive properties of programs without compromising pure functional reasoning. This thesis contributes an approach to coherently integrating cost and functional verification in the setting of dependent type theory. Inspired by the method of synthetic phase distinctions of Sterling and Harper, I explain how the internal modal type theory of (pre)sheaf categories evinces a phase distinction between a cost-sensitive phase and a function phase suitable for such an integration. At the level of programming and verification, I demonstrate the ability of the internal type theory to mediate between cost-sensitive and purely functional verification. At the level of semantics, I prove an internal, cost-sensitive version of a classical result of Plotkin’s — computational adequacy for PCF.