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 contribute an inductive logical relation to prove normalizability of all well-typed open terms. For the latter, we contribute 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.

185 pages

Thesis Committee:
Stephanie Balzer (Chair)
Robert Harper

Jignesh Patel, Interim 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