Rencontre, 23 mai 2024
Programme
- 10:30 – 12:00
-
Stelios Tsampas (FAU Erlangen-Nürnberg)
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.
- 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 non-determinism) 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 non-determinism 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 well-known that in the call-by-name λ-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in the call-by-value λ-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 well-known 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.
