Rencontre, May 23, 2024
La rencontre aura lieu en amphi B, sur le site Monod de l'ENS de Lyon (3ème étage).
Elle sera diffusée en ligne, à l'adresse suivante : https://bigbluebutton2.enslyon.fr/b/danxnb2klecy le code d'accès est 678064 à l'envers, et il faut penser à autoriser les popups.
Programme
 10:30 – 12:00

Stelios Tsampas (FAU ErlangenNürnberg)
Logical relations constitute a key method for reasoning in higherorder languages. They are usually developed on a percase 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 HigherOrder Mathematical Operational Semantics (HOMOS), a highly parametric categorical framework for modeling the operational semantics of higherorder languages. Additionally, we have developed efficient principles that simplify reasoning on logical relations for languages specified in the HOMOS 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 wellbehaved, one can automatically construct a logical relation that is sound for contextual equivalence. Examples I will be covering include unary, binary and stepindexed logical relations, for simple as well as recursive types.
 13:45 – 14:45

Maaike Zwart (IT University of Copenhagen)Invited talk: What Monads Can and Cannot Do With a Bit of Extra Time
The delay monad provides a simple way to introduce general recursion in type theory. Combining this monad with other monads then allows us to write programs in type theory that use a wide range of computational effects. In this talk I will look at two ways of combining the delay monad with monads that can be described by higher inductive types (HITs). The first way is via a distributive law, which describes the interaction between the two effects. But… such distributive laws do not always exist. In fact, I will show that there is no distributive law for combining the delay monad with the finite powerset monad (modelling nondeterminism) or the finite distribution monad (modelling probability). We therefore also look at a second way, via a free combination with no interaction between the two effects. This still gives a rich language allowing us to reason about nondeterminism and probabilistic effects in the presence of recursion.
 15:15 – 16:15

Victor Arrial (IRIF)Invited talk: Genericity Through Stratification
A fundamental issue in the λcalculus is to find appropriate notions for meaningfulness. It is wellknown that in the callbyname λcalculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in the callbyvalue λcalculus (CbV). This paper validates the challenging claim that yet another notion, previously introduced in the literature as potential valuability, appropriately represents meaningfulness in CbV. Akin to CbN, this claim is corroborated by proving two essential properties. The first one is genericity, stating that meaningless subterms have no bearing on evaluating normalizing terms. To prove this (which was an open problem), we use a novel approach based on stratified reduction, indifferently applicable to CbN and CbV, and in a quantitative way. The second property concerns consistency of the smallest congruence relation resulting from equating all meaningless terms. While the consistency result is not new, we provide the first direct operational proof of it. We also show that such a congruence has a unique consistent and maximal extension, which coincides with a wellknown notion of observational equivalence. Our results thus supply the formal concepts and tools that validate the informal notion of meaningfulness underlying CbN and CbV.
A preprint is available at https://arxiv.org/abs/2401.12212.