Kickoff meeting
The first general meeting of the IRN-LI will be held in Rome, on 12-13 May 2025. It will be joint with the inaugural session of the LYSMimpactΦ seminar, and followed by the second edition of the PACMAN workshop.
There will be two invited talks:
- Thomas Ehrhard (IRIF, Paris, France) and Laurent Regnier (I2M, Marseille, France):
- Differential linear logic: from semantics to syntax.
- Jacopo Emmenegger (DIMA, Genova, Italia):
- Categorical structures for comprehension and context extension.
- This talk is about the main categorical accounts of the set-theoretical operation of comprehension of a formula, and of the type-theoretical operation of context extension. Intuitively, the two operations are connected: in both cases we are allowed to treat the formula/type as true/inhabited. I will survey the categorical structures proposed by Lawvere, Ehrhard, Cartmell, Taylor, Pitts, Jacobs, and Dybjer to capture these operations, and report on some recent results that clarify the relationships between these structures and provide some free constructions for them. This talk is based on joint work with Greta Coraglia, and with Francesco Dagnino and Andrea Giusto.
- slides
as well as ten contributed talks.
Schedule
- Monday 12 May
- 09:00-10:30: invited talk: Thomas Ehrhard and Laurent Regnier
- 11:00-12:20: contributed talks: Rémi Di Guardia; Hugo Herbelin
- 14:00-16:00: contributed talks: Davide Barbarossa; Laura Fontanella; Emmanuel Beffara
- 16:30-18:00: general discussion
- 19:00: social dinner (same place as the meeting, ground floor)
- Tuesday 13 May
- 09:00-10:20: contributed talks: Benoît Valiron; Vladimir Zamdzhiev
- 11:00-12:30: inaugural session of LYSMimpactΦ
- 14:00-15:30: invited talk: Jacopo Emmenegger
- 16:00-18:00: contributed talks: Federico Olimpieri; Giulio Guerrieri; Adrien Ragot
Contributed talks
- Davide Barbarossa (University of Bath): On the tropical geometry of probabilistic programming languages
- In the last few years there has been a growing interest towards
methods for statistical inference based on ideas from
computational algebraic geometry, and notably from tropical
geometry, that is, the study of algebraic varieties over
the min-plus semiring. At the same time, recent works in
programming language theory demonstrated the possibility of
interpreting higher-order programs in the framework of
tropical mathematics, by exploiting the weighted relational
semantics from linear logic. I will discuss some work in
progress with Paolo Pistone, in which we try to put these
two worlds in contact by importing and adapting methods
from tropical geometry to perform statistical inference on
higher-order programs.
The starting point is that the problem of describing the most-likely behaviour of a probabilistic PCF program reduces to studying a tropical polynomial function associated with the program. Time permitting, I would discuss either, or both, an intersection type system that captures such polynomials, and the fact that the tropical polynomial associated with a probabilistic protocol expressed in our language ensures a differential privacy preservation. - slides
- Emmanuel Beffara (LIG, Université Grenoble Alpes): Learning to prove with proof assistants?
- The aim of the presentation is to discuss some ideas on the use of proof assistants to teach mathematical proof at the beginning of university. We will discuss the difference between formal proof and the practice of demonstration, the role that the proof assistant can play as an interlocutor in a demonstration process, the methods of interaction with the tool, and in the background what the proof-program correspondence can tell us about the construction of the notion of mathematical proof.
- slides
- Rémi Di Guardia (IRIF, Paris Cité): Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
- We revisit sequentialization proofs associated with the
Danos-Regnier correctness criterion in the theory of proof
nets of linear logic. Our approach relies on a
generalization of Yeo's theorem for graphs, based on
colorings of half-edges. This happens to be the appropriate
level of abstraction to extract sequentiality information
from a proof net without modifying its graph structure. We
thus obtain different ways of recovering a sequent calculus
derivation from a proof net inductively, by relying on a
splitting ⅋-vertex, on a splitting ⊗-vertex,
on a splitting terminal vertex, etc.
The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) &endash; similar results from the literature required more involved encodings. - slides
- Laura Fontanella (Université Paris Est Créteil ): Realizability models for set theory
- In the 19th century, mathematicians began to explore
fundamental questions about the foundations of mathematics.
This inquiry led to the development of formal logic, marked
by a particular focus on axiomatic systems, from which set
theory emerged as a solid foundation for all mathematics.
Around the same time, the concept of computability was
investigated in connection with the idea that mathematical
proofs should be “computable.” This line of inquiry gave
rise to Kleene's realizability.
In this talk, we will examine how these two research traditions are now converging in the field of classical realizability for set theory. We will explore the construction of models of ZF using lambda-terms and use this technique to investigate the computational content of set theory. We will present the current state of the art alongside several open problems in this area. In particular, we will show that while it is possible to realize even large cardinal axioms, the computational content of the Axiom of Choice remains elusive. - slides
- Giulio Guerrieri (University of Sussex): Strong Call-by-Value and Multi Types
- slides
- We provide foundations for strong (that is, possibly under
abstraction) call-by-value evaluation for the
lambda-calculus. Recently, Accattoli et al. proposed a
form of call-by-value strong evaluation for the
lambda-calculus, the external strategy, and proved it
reasonable for time. Here, we study the external
strategy using a semantical tool, namely Ehrhard's
call-by-value multi types, a variant of intersection
types. We show that the external strategy terminates
exactly when a term is typable with so-called shrinking
multi types, mimicking similar results for strong
call-by-name. Additionally, the external strategy is
normalizing in the untyped setting, that is, it reaches
the normal form whenever it exists.
We also consider the call-by-extended-value approach to strong evaluation shown reasonable for time by Biernacka et al. The two approaches turn out to not be equivalent: terms may be externally divergent but terminating for call-by-extended-value. - Hugo Herbelin (IRIF - INRIA): About adjunctions, sequent calculus and call-by-push-value
- We will discuss a “type-as-proposition-as-object” correspondence between adjunctions, polarized sequent calculus and call-by-push-value.
- Federico Olimpieri (Aix-Marseille Université): Linearization via Rewriting
- We introduce the structural resource λ-calculus, a new formalism in which strongly normalizing terms of the λ-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its linearization. The calculus is shown to be normalizing and confluent. Noticeably, every strongly normalizable λ-term can be represented by a type derivation. This is the first example of a system where the linearization process takes place internally, while remaining purely finitary and rewrite-based.
- slides
- Adrien Ragot (UPSaclay / LMF): Parsing Correctness Criteria for second order linear logic
- We present a novel correctness criterion for Second Order
Multiplicative Linear Logic proof structures (MLL2).
The first question we need to tackle is how to
represent proof structures, our choice the (quite
standard) idea of syntax trees with axioms linking dual
formulas, however since we consider untyped proof
structures, this alone is not enough to handle
quantifiers properly. Our solution is to add pointers:
some which capture the information of the existential
witnesses and others capturing proper variables of
universal quantifiers.
Our criterion is based on parsing: a rewriting on proof structures which (on proof nets) corresponds to steps of anti-proof search. To properly define the parsing rewriting it will be necessary to consider daimon links which can be understood as generalised axioms, then the criterion may be stated as such: a proof structure S is a proof net if and only if S rewrites (for the parsing reduction) to a single daimon link.
Because the rewriting is confluent on proof nets and a step of parsing rewriting always reduce the number of links in a proof structure the naive implementation of this correctness criterion runs in quadratic time. - slides
- Benoit Valiron (UPSaclay / LMF): Quantum lambda-calculus : Realizability and emerging logical properties
- In this talk, we first present a naïve quantum lambda-calculus with an operational semantics. We then develop a realizability semantics from the behavior of terms, and discuss the logical framework that naturally emerges from the system.
- slides
- Vladimir Zamdzhiev (Inria): Operator Spaces, Linear Logic and the Heisenberg-Schrödinger Duality of Quantum Theory
- In this talk we recall how quantum operations (also known as
channels) are modelled mathematically in both the
Heisenberg and Schrödinger pictures of quantum theory. The
two pictures are dual to each other and we recall how the
theory of operator spaces can be used to describe this
duality in mathematical terms. Operator spaces, studied in
noncommutative geometry, are the noncommutative (or
quantum) analogue of Banach spaces. We prove that the
category OS (operator spaces with complete contractions as
morphisms) is locally countably presentable and a model of
Intuitionistic Linear Logic in the sense of Lafont. We then
describe a model of Classical Linear Logic, based on OS,
whose duality is compatible with the Heisenberg-Schrödinger
duality of quantum theory. In the later model, the
mathematical descriptions of systems in the Heisenberg
picture correspond to formulas with negative logical
polarity, whereas those in the Schrödinger picture
correspond to formulas with positive logical polarity.
Joint work with Bert Lindenhovius. - slides
Venue
Università degli Studi “Roma Tre” Argiletum, Via della Madonna dei Monti, 40 Roma.