A Beginner's Guide to Logical Relations for a Logical Framework (group-internal talk)

Logical relations are an established proof technique for deriving meta-level theorems of formal systems. For example, they have been used to prove strong normalization, type safety, and correctness of compiler optimizations in the setting of various type theories and lambda calculi. Theories of logical relations have been stated for a wide range of formal systems.

To formalize formal systems themselves, logical frameworks have been sucessfully used, particularly shining when specifying syntax and deduction (e.g. using judgements-as-types and higher-order abstract syntax). And odule systems over logical frameworks allow to modularly identify, translate, and combine full hierarchies of formal systems.

How to represent logical relations in such systems is an ongoing research question. In “Logical Relations for a Logical Framework” (ACM Transactions on Computational Logic (2013)), Rabe and Sojakova present a theory of logical relations applicable in the setting of logical frameworks that, when instantiated for formal systems formalized therein, gives a reasonable notion of logical relations within those systems.

We provide a detailed exposition of a special case, accessible to everyone familiar with basics of formalizing in logical frameworks. Our exposition is embedded in a coherent narrative spanning from concretely motivating logical relations (by walking through a proof of strong normalization for the simply-typed lambda calculus) up to concretely modeling a corresponding language feature for the Mmt module system over the Edinburgh Logical Framework. The mechanics of our derived language feature are novel and forgo the need of introducing any logical relation-specific language primitive.