Stelios Tsampas (FAU Erlangen-Nürnberg), Logical Relations in Higher-Order Mathematical Operational Semantics

Programme

Résumé

Logical relations constitute a key method for reasoning in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the problem setting. In recent work, we have introduced general constructions of logical relations at the level of Higher-Order Mathematical Operational Semantics (HO-MOS), a highly parametric categorical framework for modeling the operational semantics of higher-order languages. Additionally, we have developed efficient principles that simplify reasoning on logical relations for languages specified in the HO-MOS framework. In this presentation, I will be dissecting logical relations to expose their coalgebraic core, and explain how our theory uncovers the lightweight reasoning principles hidden underneath the surface. For instance, within this framework, if a given operational semantics is sufficiently well-behaved, one can automatically construct a logical relation that is sound for contextual equivalence. Examples I will be covering include unary, binary and step-indexed logical relations, for simple as well as recursive types.