General meeting 2026

The next general meeting of the IRN LI will be held in at the ENS de Lyon, on 23-24 June 2026. It will be followed by the 25 June edition of the Chocola seminar.

Registration for both events is free and mandatory, and includes lunches and coffee breaks (but not dinners nor accommodation). Registration for the general meeting of the IRN is now closed. Registration for Chocola is managed separately (deadline: 18 June).

Talks will be broadcast online, via BBB. Instructions will be available here shortly before the meeting.

Invited speakers

Programme

Tuesday 23 June
10:30-11:00: welcome coffee
11:00-12:30: invited talk: Fabien Carbo-Gil
12:30-14:00: lunch break
14:00-15:30: contributed talks: Antonio Piccolomini d’Aragona, Gabriele Vanoni
15:30-16:00: coffee break
16:00-17:30: invited talk: Melissa Antonelli
Wednesday 24 June
09:00-10:30: invited talk: Laura Fontanella
10:30-11:00: coffee break
11:00-12:30: contributed talks: Loïc Allègre, Adrien Ragot, Alexis Saurin
12:30-14:00: lunch break
14:00-15:30: general discussion
15:30-16:00: coffee break
16:00-17:30: contributed talks: Raffaele Di Donna, Rémi Di Guardia, Christian Retoré

Talks

Loïc Allègre (LIRMM, Université de Montpellier): First-order Intuitionistic Multiplicative Linear Logic with Hilbert’s Epsilon
Hilbert's Epsilon Calculus is an alternative way to express logical quantification, by extending a chosen logical language with the epsilon operator, forming terms from formulae. It has mostly been historically studied in the framework of first-order classical logic, where it can be used to replace the traditional quantifiers ∀ and ∃, and has the interesting property of enabling non-elementary compression of cut-free proofs.
Our work aims to study the addition of the epsilon operator to Linear Logic, more specifically to Intuitionistic Multiplicative Exponential Linear Logic (IMELL). This represents a novel approach to first-order multiplicative linear logic that could prove interesting, especially since the usual ∀ and ∃ remain very much additive by their nature.
Alongside the relatively straightforward integration of epsilon rules to proof systems, we also propose categorical semantics for first-order IMELL with Hilbert's epsilon, in the form of hyperdoctrines (as defined by Lawvere) in which the image posets are ordered monoids (which can be seen as monoidal closed categories) equipped with a comonad to interpret the exponential "!".
Joint work with Fabio Pasquali (University of Milan) and Christian Retoré (LIRMM, University of Montpellier).
Melissa Antonelli (Universität Tübingen): Towards a unified perspective in circuit complexity via discrete ODEs
In this talk I will introduce a new perspective on the study of small circuit classes. The crucial novelty is the introduction of original recursion schemas defined in terms of discrete ordinary differential equations (ODEs). Based on this, we have obtained a uniform framework to characterize multiple circuit classes, ranging from the basic class of functions computable by unbounded boolean circuits of polynomial size and constant depth (FAC⁰) to circuits with bounded fan-in gates and logarithmic depth (FNC¹), also including gates allowing for various counting operations. Additionally, this new approach has revealed an inherent relationship between computation performed by discrete ODEs and resources in circuit complexity, which certainly deserves further attention.
(Main results are part of joint works with A. Durand & J. Kontine, and A. Durand & R. Li)
Fabien Carbo-Gil (CGGG, Aix Marseille): Du concept de calcul au problème du continu : La dialectique du formel et de l’informel chez Gödel
Les travaux de Turing ont participé à donner aux théorèmes d’incomplétude de Gödel toute leur portée en fournissant une définition explicite de la notion de système formel.
Au-delà de ce résultat, Gödel qualifie la caractérisation du concept de calcul par les machines de Turing de véritable « miracle », puisqu’il constitue un exemple inédit de caractérisation « absolue » d’un concept.
La réflexion autour de la possibilité d’étendre le succès de l’analyse de Turing du concept de calcul au concept d’ensemble est au cœur de la réflexion de Gödel sur l’axiomatique ensembliste. Nous tenterons dans cette présentation de dessiner les contours de la dialectique entre formalisation et réflexion informelle qui est au cœur de son interprétation des théorèmes d’incomplétude ainsi que de l’analyse conceptuelle du concept d’ensemble qu’il cherchera à développer par la suite.
Cette analyse prend notamment comme point focal les limites des systèmes formels, à commencer par les problèmes indécidables tels que l’Hypothèse du continu.
Nous terminerons par quelques remarques concernant la pertinence de ce cadre de réflexion pour comprendre certains développements récents de la théorie des ensembles concernant le problème du continu et les débats à propos des nouveaux axiomes de la théorie des ensembles.
Raffaele Di Donna (Université Paris Cité, Università Roma Tre / IRIF): Connectivity in proof-nets: from classical to intuitionistic linear logic and the bang calculus
I will give you an overview of my recent work on linear logic proof-nets. The common thread is the study of the structural, geometric properties of proofs, and how they are related to the purely logical properties, with particular emphasis on the property of connectivity. I will present some interesting results from two related lines of research on classical and intuitionistic linear logic, and on the connection between proof-nets and the bang calculus.
Rémi Di Guardia (Inria / IRIF): No Uniform Interpolation for Linear Logic
Few results are known on uniform interpolation for linear logic, the main one being that Multiplicative-Additive Linear Logic has the uniform interpolation property (and so does its intuitionistic variant) [Alizadeh, Derakhshan, Ono 2014]. We present a simple counter-example to this property for formulas of Multiplicative-Exponential Linear Logic (and its intuitionistic variant).
Laura Fontanella (LACL, Paris Est Créteil): Ordinals in classical realizability models
Classical realizability, introduced by Krivine, provides a computational interpretation of classical logic and a powerful framework for constructing models of set theory. In the first part of this talk, I will present the general architecture of Krivine's classical realizability and the main ingredients involved in the construction of realizability models. I will then discuss several ways of representing ordinals in classical realizability models and explain how these representations are important for realizing fragments of the Axiom of Choice. In the final part of the talk, I will address the problem of cardinal preservation in classical realizability models. I will present a transfinite generalization of bar recursion and show how it can be used both to preserve cardinals and to realize fragments of the Axiom of Choice.
Antonio Piccolomini d'Aragona (Eberhard Karls Universität Tübingen): A contribution to the history of the Curry-Howard correspondence: Prawitz's 1968 homomorphism
I survey Dag Prawitz's "Constructive semantics", published in 1970, but drawn from a talk of 1968, where Prawitz defines a homomorphism between Natural Deduction derivations for minimal or intuitionistic first-order logic, on the one hand, and a system of typed construction terms similar to typed lambda-calculus on the other.
Prawitz starts by providing types, and by assigning them to certain construction objects, as well as to formulas of a first-order language. Next, he introduces a notion of construction of a formula. He then builds a language of construction terms, also typed, and defines denotation of terms relative to assignments of individuals and constructions to free typed variables. Prawitz takes finally into account natural deduction calculi for minimal and intuitionistic first-order logic, and proves soundness for both on the language of construction terms. The proof boils down to the definition of the above told mapping from derivations to construction terms. The mapping preserves the typing of assumptions and conclusions, as well as standard normalisation procedures as a kind of beta-conversion for construction terms.
Prawitz's morphism predates by one year William Howard's "The formulae-as-types notion of construction", so it can be said to anticipate what came to be known as the Curry-Howard isomorphism. Compared to the latter, however, Prawitz's correspondence has different intentions and goals. A further aim of my talk is thus to discuss these divergences, and hint at those they forerun in subsequent developments of both Prawitz's work and the Curry-Howard legacy.
Adrien Ragot (Université Sorbonne Paris Nord & Università degli studi Roma tre): Partial Algebra and semantic analysis
In compiler design, semantic analysis sits at the end of the frond-end of a compiler: it transforms an abstract syntax tree (AST) into an elaborated term - i.e. typed term, a typed or annotated AST, an elaborated term together with typing derivation, etc...
Semantic analysis is not always successful, it can reject some ASTs resulting in a compilation error: for instance, when it involves forms of type checking or type inference algorithms it rejects an AST if it can not be typed.
Semantic analysis should be easy to reverse, given an elaborated term, forgetting the 'elaboration' yields back the original AST or term. It is clear that all ASTs are not the image of some elaborated term under the forgetful map (since for instance some programs fail type checking). An AST successfully passes semantic analysis if and only if it is the image under the forgetful map of an elaborated term.
We propose a general framework in which one can study the previous question, specifically designed for type-driven semantic analysis. In particular we study partial indexed magmas, which turned out to be a simple yet meaningful and non-trivial setting. For instance morphisms may enjoy two key properties of soundness and completeness. Furthermore some class of terms called generated terms are identified and can be characterised by a rewriting called coalescence which always terminates.
A key theorem is proven: if a morphism f from A to B is sound and complete, the image under f of the generated terms in A corresponds exactly to the generated terms in B. Thus when: f corresponds to the forgetful map of a semantic analysis, the generated terms in A are the elaborated terms, while B is the set of ASTs, this gives a way to ensure that an AST successfully passes the semantic analysis.
In particular, one can test by coalescence in B if an element is generated in B and thus if it successfully passes semantic analysis (since in that case it is the image under the forgetful map f of an elaborated term i.e. a generated term in A). Therefore coalescence provides a way to implement the semantic analysis phase of a compiler, and the algebraic framework we introduce allows to verify (eventually in a theorem prover) the correctness of a semantic analysis pass.
Indexed partial magmas can be specialised into Residual magmas in which one can study the confluence of coalescence rewriting. This is particularly relevant because coalescence rewriting always terminates, if it is furthermore confluent, there is no need for a specific strategy to test whether a term reduces to a specific element. This makes the coalescence criterion (does the term reduce to a specific term t0) efficient and actually useable. We will see that the 1-1 confluence of coalescence can be characterised by purely algebraic properties: 2-cancellativity and right-explicitness.
Christian Retoré (Université de Montpellier LIRMM): Oldies but Goodies? Proof Nets as Edge‑Coloured Graphs
In this talk, I’ll revisit a few old but still rather useful ways of representing multiplicative proof nets as unlabelled, edge‑coloured graphs, where certain cycles are ruled out so that the graphs can be broken down step by step. This property, called sequentialisation, mirrors the rules of the sequent calculus.
The first version, aggregates (A), dates back to 1993. Axioms are vertices and tensor links are complete bipartite graphs, each given a colour, with the condition that there be no cycle containing at most one edge of any colour.
A second style, RnBc (1996), takes formulas as cographs and axioms as perfect matchings. It can be seen as arising from the RnBl graphs—close to the well‑known Danos–Regnier proof nets—via folding and unfolding constructions, and both RnBc and RnBl turn out to behave very well for pomset logic.
A third version, RnBl (also 1996), consists of a class of edge‑bicoloured graphs coinciding with the Danos–Regnier construction, expressed in graph‑theoretical terms. One colour forms a perfect matching, the other describes the links, and the key condition is the absence of alternating cycles. Sequentialisation follows via either Danos’ splitting of par or Girard’s splitting of times.
I will also explain a connection between aggregates and RnBc, which has never been written down or presented before and goes back to discussions with Jean‑Claude Bermond in the mid‑1990s. I will close by showing how this correspondence allows one to return from RnBc to aggregates and to approach some questions in pomset logic. This is work in progress, but I believe it has very good chances of success.
Alexis Saurin (IRIF): Interpolation de réseaux avec coupures
L'interpolation de Craig (et ses variantes) se démontre d'habitude sous hypothèse de prouvabilité sans coupure.
Je présenterai comment on peut obtenir un résultat plus fin, où on n'interpole plus des jugements A ⊢ B mais des preuves de ces jugements.
Dans M(E)LL, on obtient ainsi une interpolation au niveau des réseaux: Si R est un réseau de conclusions A,B, on obtient (i) une formule C dans le langage commun à A et B et (ii) des réseaux R1, R2 de conclusions respectives A, C et C^⊥, B tels que la composition de R1 et R2 est équivalente à R.
Je discuterai notamment du rôle de la coupure dans ce résultat et de la relation entre cette construction et les critères de parsing et de contractibilité.
(À partir de travaux en cours avec Fiorillo, Le Boulc'h, Osorio et Pellissier.)
Gabriele Vanoni (Université Paris Cité): The ω-CPO of Intersection Type Derivations
Non-idempotent intersection type systems provide a quantitative account of evaluation in the λ-calculus: they track resource usage, characterize normalization, and relate type derivations to the operational and denotational semantics. This correspondence, however, is essentially finitary. Standard systems describe terminating computations through finite type derivations, and do not directly account for divergence.
We develop an approximation-based approach to infinitary typing. We extend the standard call-by-name non-idempotent intersection type system to cover diverging computations. Interestingly, it is enough to add a special axiom for λ-abstractions that assigns coarse types, yielding finite partial type derivations. These derivations act as finite approximants of infinitary ones and can be progressively refined by unfolding abstractions and enriching the surrounding typing information. To organize this refinement process, we define an order on partial derivations based on ordered intersections and the persistence of derivation nodes.
This way, allowing for infinite intersection types, we are able to show that increasing sequences admit a limit, and thus that all terms are typable without using the new axiom, but possibly having infinitary type derivations."

Venue

Amphithéâtre B (3rd floor), ÉNS Lyon, 46 allée d’Italie, Monod Campus, Lyon, France (directions). Beware: Monod ≠ Descartes !.

Some hotel suggestions:

close to the venue:
IBIS Gerland Mérieux
IBIS Lyon Gerland Musée des Confluences
Mob Hotel Confluence
Appart City Gerland
a bit further away but close to transport stations
Odalys City Confluence
Adagio Access Lyon Centre Université - Rue Chevreul

Participants

Organizing committee

Paolo Pistone (local organizer), Lorenzo Tortora de Falco, Lionel Vaux Auclair