5th Year M.S. Thesis Presentation - Rui Li
July 30, 2026 3:00PM—4:20PM
Location:
In Person
-
Blelloch-Skees Conference Room, Gates Hillman 8115
Speaker:
RUI LI,
Master's StudentComputer Science DepartmentCarnegie Mellon University
Logical relations are a powerful proof technique for establishing properties of programming languages. Traditionally, they are defined by induction on the structure of types, with each case specifying the meaning of computability at the corresponding type. This enables a robust methodology for program verification, as one proves that programs satisfy the computability associated with their types. In this thesis, we present an alternative, purely inductive formulation of logical relations using inference rules. To illustrate the broad applicability of the inductive formulation, we apply it to two calculi: the simply-typed lambda calculus and a process calculus based on intuitionistic linear logic session types. For the former, we use an inductive logical relation to prove normalizability of all well-typed open terms. For the latter, we use another inductive logical relation to prove termination of all closed, well-typed session programs. Together, these results demonstrate that inductive logical relations offer a promising alternative to traditional formulations.
Thesis Committee
Stephanie Balzer (Chair)
Robert Harper
Additional Information
For More Information:
amalloy@cs.cmu.edu