Doctoral Speaking Skills Talk - Harrison Grodin
— 1:00pm
Location:
In Person
-
Gates Hillman 8102
Speaker:
HARRISON GRODIN
,
Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.harrisongrodin.com/
Friday, November 21, 2025, 12 – 1pm
Software development depends on the use of libraries whose public specifications inform client code and impose obligations on the private implementation; it follows that any approach to verification at scale must also be modular, preserving such abstraction. Hoare's influential methodology for such verifications uses an abstraction function to demonstrate the coherence between an implementation and its specification.
For all of its influence, the Hoare methodology relies on conventional separation between implementation and specification, providing no linguistic support for ensuring that these conventions are obeyed. We present a synthetic account of Hoare's methodology within dependent type theory, encoding the data of an abstraction function within types themselves. Accordingly, various foundational principles are rendered as theorems: for example, a noninterference theorem characterizes an internal notion of modularity guaranteed by the theory.
Moreover, this approach scales to permit the specification and verification of the cost of programs, allowing clients to verify their own cost relative to a specification. To maintain abstraction, the implementation must be merely upper bounded in cost by the specification, which is achieved via a novel "sealing" effect. The resulting type theory supports modular development of programs and proofs in a manner that hides private details while permitting modular verification of both the cost and behavior of programs.
Presented as part of the PLunch Seminar
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement
For More Information:
matthewstewart@cmu.edu