Logical Relations, Fibrations, and Definability for Call-by-Value Languages
University of Oxford
Abstract:
Logical relations are a versatile tool for studying programming languages, with the so-called 'fundamental lemma' characterising the interpretations of terms as exactly those that satisfy every logical relation. In this talk I will explore these ideas in the setting of an effectful programming language à la Moggi's computational lambda calculus.
Starting from a categorical model of an effectful programming language (in the style of Moggi's computational lambda calculus), I will study three inter-related questions, roughly corresponding to the three terms in the title:
1. How can one prove properties of the semantics?
2. How can one refine the model to ensure morphisms only satisfy certain properties?
3. How can one characterise the morphisms that are the interpretation of some term?
Finally, I will indicate how one can put together these three components to construct a model in which every morphism is definable.
Joint work with Ohad Kammar and Shin-ya Katsumata.