The 2025 PPS Days will take place from Tuesday, July 1 to Thursday, July 3. In particular they will contain:

• a general meeting of PPS on July 2, at 16:00,
• an invited talk by Guy McCusker on July 3, at 10:00.

They will mainly be located in the Pierre-Gilles de Gennes amphitheater of Université Paris Cité, Condorcet building. To find the amphitheater:

• Like labyrinths? try to reach it from the basement of the Condorcet building!
• Otherwise, in the patio of the building (via rue Hélène Brion) take the stairs on your left, without entering the building.

Coffee

15:00 — Introduction

15:15 — Rémi Di Guardia : Identity of Proofs and Formulas in Linear Logic (slides)

In a logical system, deciding whether two proofs, or two formulas, are equal is often complicated. Indeed, one usually does not want to identify only proofs that are syntactically equal, i.e. whose rules are exactly the same. In many sequent calculi, there is a cut rule that allows for computation - through a process called cut-elimination - and one wishes for two proofs related by such a computation to be equivalent. Looking at programs through the Curry-Howard correspondence, even if 2 + 2 and (1 + 2) + 1 are not strictly the same term, it is still very sensible to identify them. Another notion of identity on proofs is axiom-expansion, corresponding to the fact that a function f should be considered the same as x ↦ f(x), the function that takes an input x and returns f(x), which is again very natural to ask for. Hence, proofs are seen as equivalent up to these two relations (at least), which in many logical systems is either a trivial nonsense or a combinatorial nightmare. Furthermore, these equalities between proofs yield a notion of equality between formulas, called isomorphism. Two formulas A and B are isomorphic if there are proofs between them whose compositions yield identities - up to the above equivalence relations. Intuitively, this means there is a loseless encoding between A and B, and thus they can be considered as the same; for instance, every use of A can be replaced with one use of B. I will present and give a survey of these two problems of equalities in the framework of linear logic.

16:00 — Éléonore Mangel : Classical notions of computation and the Hasegawa-Thielecke theorem (slides)

In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus. A main challenge in designing a denotational semantics is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. Building on the work of the third author, we devise the notion of dialogue duploid, which provides a non-associative and effectful counterpart to the notion of dialogue category introduced by the second author in his 2-categorical account, based on adjunctions, of logical polarities and continuations. We show that the syntax of the polarised calculus can be interpreted in any dialogue duploid, and that it defines in fact a syntactic dialogue duploid. As an application, we establish, by semantic as well as syntactic means, the Hasegawa-Thielecke theorem, which states that the notions of central map and of thunkable map coincide in any dialogue duploid (in particular, for any double negation monad on a symmetric monoidal category).

16:30 — Adrienne Lancelot : Mirroring Call-by-Need, or Values Acting Silly (slides)

Call-by-need evaluation can be seen as combining the best of call-by-name and call-by-value (duplicating only values and erasing anything). We study the dual evaluation paradigm and name it call-by-silly for its blatant inefficiency. I will try to convince you it is still relevant to study and reveal the dark side of call-by-value…

Coffee

10:00 — Gabriele Vanoni : Infinitary Intersection Typing via Geometry of Interaction (slides)

The λ-calculus serves as the de facto standard mathematical model for programming languages, with intersection type systems providing a compositional approach to understanding operational properties of λ-terms. While traditional intersection types characterize termination, non-idempotent intersections refine this connection by tracking resource usage, leading to a quantitative understanding of evaluation. In particular, they provide a way to analyze the complexity of normalization, measure the number of reduction steps, and establish fine-grained correspondences between typing and execution. However, existing techniques inherently rely on finiteness: they are well-suited for analyzing terminating computations but struggle to capture the behavior of non-terminating processes, such as those arising in interactive or infinite computations. To overcome this limitation, we introduce a novel approximation technique based on finite representations of infinite type derivations. Rather than working directly with infinite objects, we construct a sequence of finite approximations that capture progressively larger portions of the computational behavior of a λ-term. By ensuring that these approximations form an increasing chain, we can recover the full infinite derivation as their limit. To do this, we use techniques based on Girard's geometry of interaction. These techniques not only provide a clean and constructive way to extract finite approximations, but also allow us to extend intersection types beyond termination, enabling us to reason about arbitrary reduction sequences.

10:45 — Pierre Letouzey : Calculs de discrépance pour des fonctions de Hofstadter (slides)

11:30 — El-Mehdi Cherradi : Bridging type theory and categorical logic, a story of coherence (slides)

Although type theory and category theory can be thought of as two distinct frameworks for studying logic and reasoning, the connection between the two has been fruitfully studied, in particular under the angle of the Curry-Howard-Lambek correspondence. There is, however, a key difference between the two perspectives: while type theory relies importantly on equality between types and terms, category-theoretic constructions usually involve a universal property, defining them only up to (unique) isomorphism. Thus, understanding how to navigate from coherent isomorphisms to identities is a critical step to bridge the gap between type theory and category theory. In the the first part of this talk, I will propose a historical account of this so-called coherence issue, whereas the second part will be devoted to my contributions to its homotopy-enabled counterpart, comparing homotopy type theory and (∞,1)-category theory.

Lunch in front of the Sophie Germain building

14:30 — Vincent Moreau : Profinite clones and trees (slides)

An observation at the heart of algebraic language theory is that regular languages of finite words are exactly the languages recognized by finite monoids. In the same way, abstract clones provide an appropriate notion of algebra for regular languages of finite trees (with sharing). Inspired by Stone duality and the topological approach to recognition, we define the profinite completion of clones as a codensity monad with respect to finite clones. Using the notion of parametric right adjoint, we show that it generalizes both the ultrafilter monad and the profinite completion of monoids. Moreover, by taking profinite completions of clones of trees, we get a notion of profinite tree that we prove to coincide with profinite lambda-terms of Church types.

14:55 — Moana Jubert : Towards a definition of indexed presheaves (slides)

15:20 — Thomas Ehrhard : Surprise! 🎉

16:00 — PPS general assembly

Coffee

10:00 — Exposé invité — Guy McCusker (U. Bath) : Imperative Taylor Expansion (slides)

The 2024 Alonzo Church Award honoured Ehrhard and Regnier’s body of work on differential lambda calculus and the Taylor expansion of lambda-terms. This powerful technique provides a new approximation theory for functional programs, which understands lambda-terms as formal sums of terms of a linear “resource calculus”. In the resource calculus, ordinary application — in which a term may duplicate or erase its arguments — is replaced by a linear application of terms to multisets of arguments.

We explore what happens if the multisets of the resource calculus are replaced by lists, making application order-sensitive. The resulting calculus provides a target for a Taylor expansion of higher order imperative programs with local variables, giving an interpretation of Reynolds’s “Syntactic Control of Interference” (SCI) as formal sums of resource calculus terms.

This is joint work with Pierre Clairambault and Lionel Vaux Auclair.

11:10 — Quentin Aristote : Monotone Weak Distributive Laws over the Lifted Powerset Monad in Categories of Algebras (slides)

In both the category of sets and the category of compact Hausdorff spaces, there is a monotone weak distributive law that combines two layers of non-determinism. Noticing the similarity between these two laws, we study whether the latter can be obtained automatically as a weak lifting of the former. This holds partially, but does not generalize to other categories of algebras. We then characterize when exactly monotone weak distributive laws over powerset monads in categories of algebras exist, on the one hand exhibiting a law combining probabilities and non-determinism in compact Hausdorff spaces and showing on the other hand that such laws do not exist in a lot of other cases.

11:35 — Discussion : Les cultures scientifiques de PPS

Animated by Hugo Herbelin.

The PPS days are organised by Hugo Herbelin and Rémy Cerda.