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.

148 pages

Thesis Committee:
Robert Harper (Chair)
Jan Hoffmann
Stephen Brookes
Jonathan Sterling (University of Cambridge)
Neel Krishnaswami (University of Cambridge)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu