Rencontre, 14 décembre 2023

Programme

10:30 – 12:00

Marianna Girlando & Sonia Marin (University of Amsterdam and University of Birmingham)

Invited talk: Decidability of intuitionistic S4: a proof theoretic algorithm

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 counter-model, 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é Aix-Marseille)

Invited talk: Extensional Taylor Expansion

We introduce a calculus of extensional resource terms. These are resource terms à la Ehrhard-Regnier, 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 (non-necessarily normal) finite approximants of Nakajima trees, much like ordinary resource terms are approximants of Böhm-trees. Indeed, we show that the equivalence induced on λ-terms by the normalization of extensional Taylor-expansion 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 order-based 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 well-chosen reflexive object in the relational model of the λ-calculus.

This is joint work with Lison Blondeau-Patissier and Pierre Clairambault.

https://arxiv.org/abs/2305.08489