Unary Logical Relations

or: Logical Predicates--- can be used to prove: • strong normalization • type safety (high-level and low-level languages) • soundness of logics Essential idea: • A program satisfies a property if, given an input that satisfies the property, it returns an output that satisfies the property Binary Logical Relations Proof method that can be used to prove: • equivalence of modules / representation independence • noninterference in security-typed languages • compiler correctness Essential idea: • Two programs (same language or different languages) are related if, given related inputs, they return related outputs Earliest Logical Relations... • Tait ’67: prove strong normalization for Gödel’s T • Girard ’72: prove strong normalization for System F (reducibility candidates method) • Plotkin ’73: Lambda definability and logical relations • Statman ’85: Logical relations and the typed lambda calculu