Rencontre, Dec. 14, 2023
Nous serons en salle 435, au 4ème étage du site Monod de l'ENS de Lyon.
Programme
 10:30 – 12:00

Marianna Girlando & Sonia Marin (University of Amsterdam and University of Birmingham)
Intuitionistic S4 (IS4) is one of the intuitionistic variants of modal logic S4. Its semantics was defined by Fisher Servi in terms of birelational models, and it comprises two reflexive and transitive accessibility relations: one corresponding to the accessibility relation of modal logic S4 and the other corresponding to the order relation of intuitionistic Kripke frames. The question of whether IS4 is decidable has been open for almost 30 years, since Simpson posed it in his PhD thesis. We show that IS4 is decidable by performing proof search in a fully labelled sequent calculus for IS4, closely matching the birelational semantics. Our search algorithm outputs either a proof or a finite countermodel, thus additionally establishing the finite model property for intuitionistic S4.
In this talk, I will first introduce IS4 and discuss the strategies to establish decidability through proof search in the modal and intuitionistic case. Then, I will sketch the main ingredients of our proof search algorithm.
This talk is based on joint work with Roman Kuznets, Marianela Morales and Lutz Straßburger
A preprint is available here: https://arxiv.org/abs/2304.12094
 13:45 – 14:45

Paige Randall North (Utrecht University)Invited talk: Coinductive control of inductive data types
In classical programming language theory, characterizing data types as initial algebras of an endofunctor that represents a specification of the data types is an important tool. In this work, we observe that the category of algebras of such an endofunctor is often enriched in its category of coalgebras. This enrichment carries strictly more information than the traditional, unenriched category. For example, when considering the endofunctor whose initial algebra is the natural numbers, we find that the enrichment encodes a notion of 'partial' homomorphism, while the unenriched category encodes only `total' homomorphisms. We can also leverage this extra information to generalize the notion of initial algebras, following the theory of weighted limits.
Joint work with Maximilien Péroux: arXiv:2303.16793
 15:15 – 16:15

Lionel Vaux Auclair (Université AixMarseille)Invited talk: Extensional Taylor Expansion
We introduce a calculus of extensional resource terms. These are resource terms à la EhrhardRegnier, but in infinite ηlong form, while retaining a finite syntax and dynamics: in particular, we prove strong confluence and normalization.
Then we define an extensional version of Taylor expansion, mapping ordinary λterms to sets (or infinite linear combinations) of extensional resource terms: just like for ordinary Taylor expansion, the dynamics of our resource calculus allows to simulate the βreduction of λterms; the extensional nature of expansion shows in that we are also able to simulate ηreduction. In a sense, extensional resource terms form a language of (nonnecessarily normal) finite approximants of Nakajima trees, much like ordinary resource terms are approximants of Böhmtrees. Indeed, we show that the equivalence induced on λterms by the normalization of extensional Taylorexpansion is nothing but H∗, the greatest consistent sensible λtheory.
Taylor expansion has profoundly renewed the approximation theory of the λcalculus by providing a quantitative alternative to orderbased approximation techniques, such as Scott continuity and Böhm trees. Extensional Taylor expansion enjoys similar advantages: e.g., to exhibit models of H∗, it is now sufficient to provide a model of the extensional resource calculus. We apply this strategy to give a new, elementary proof of a result by Manzonetto: H∗ is the λtheory induced by a wellchosen reflexive object in the relational model of the λcalculus.
This is joint work with Lison BlondeauPatissier and Pierre Clairambault.