Logic and Logical Relations

Edmund Robinson

Abstract

Logical relations have proved a fertile ground for generalisations, mostly fairly ad hoc. These generalisations have in turn inspired attempts to furnish a general formulation of the constructions. Most of these have been based on variants of the categorical theory of relations. Work by Hermida, however, makes precise an interesting connection with formal logical systems. This has the advantage of connecting the logical relations directly with systems for reasoning about the types involved. This talk will discuss that connection, and some more recent developments arising from it.