Thesis Oral Defense - Yue Niu

— 12:00pm

Location:
In Person - Gates Hillman 8102

Speaker:
YUE NIU, Ph.D. Candidate, Computer Science Department, Carnegie Mellon University
https://yuesforest.com/index.xml

Cost-sensitive Programming, Verification, and Semantics

Computational cost is a fundamental aspect of the behavior of computer programs. However, existing program verification techniques do not simultaneously provide both faithful representation of cost structure and a way to reason about the pure functional meaning of cost-instrumented programs. 

This thesis introduces a logical framework for integrating cost-sensitive and functional program verification and semantics by means of the internal modal type theory of presheaf categories, an approach to programming language semantics first introduced by Sterling and Harper in the context of program modules and data abstraction. I demonstrate that a range of common algorithms can be formulated and formally verified to meet both their functional and cost specifications within the framework. Lastly, I extend the logical framework and use it as a metalanguage for studying the cost semantics of programming languages, culminating in an internal cost-sensitive computational adequacy theorem for PCF that relates the denotational and operational cost semantics in the style of Plotkin. 

Thesis Committee: 

Robert Harper (Chair)
Jan Hoffmann
Steve Brookes
Jon Sterling (University of Cambridge)
Neel Krishnaswami (University of Cambridge)

Event Website:
https://csd.cmu.edu/calendar/thesis-oral-defense-yue-niu