Logical Relations As Types

by Jon Sterling

• When: Friday, 30/04/2021, between 1pm and 2pm EDT (5pm - 6pm UTC)
• Where: Zoom; Outside guests please RSVP by emailing Harley Eades
• YouTube Stream/Recording: https://youtu.be/AEthjg2k718

Abstract

This is joint work with Robert Harper.

How do you prove that two implementations of an abstract type behave the same in all configurations? Reynolds famously employed logical relations to establish such results; roughly, a logical relation is a structure-respecting relation between two interpretations of a theory that evinces, in the base case, a desirable invariant.

We present a synthetic way to understand and interact with logical relations, related to classical logical relations in the same way that Euclidean geometry relates to point-sets. Previously a logical relation was defined in terms of the (complicated) details of how it is constructed as a certain kind of relation over syntax. We instead take the simpler view that everything in sight is a logical relation, and then use modalities to isolate those logical relations that are degenerate in either the syntactic or the semantic direction.

Our “logical relations as types” principle has led to a new account of modules and representation independence (S., Harper), as well as the first proofs of normalization for cubical type theory (S., Angiuli) and general multi-modal dependent type theory (Gratzer).