Giulio Guerrieri (chair)

University of Sussex

Gluing resource proof-structures: inhabitation and inverting the Taylor expansion.

A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing (and deciding in the finite case) those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.

This is joint work with Luc Pellissier and Lorenzo Tortora de Falco.

Matteo Acclavio

University of Sussex

Proof nets for the Pi-Calculus

In this talk, we discuss the syntactic limitations of syntaxes modelling programs executions in presence of interleaving concurrency, and we provide a novel approach to the problem based on applications of results on proof equivalence.

For this purpose, we recall the system PiL, an extension of first order multiplicative additive linear logic with a non-commutative non-associative connective, and nominal quantifiers, and we provide two syntaxes for proof nets extending conflict nets and slice nets. Then, use the correspondence between computation trees for the pi-calculus and derivations in the system to show how these proof nets equate derivations encoding computation trees modulo certain permutations of transitions in the operational semantics. We conclude by outlining potential research directions and applications of this approach.

This talk is based on joint work with Giulia Manara

Paolo Pistone

Université Claude Bernard Lyon 1

The Lambda Calculus is Quantifiable

We explore a few quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains. First, we study quantitative variants, based on program distances, of sensible equational theories for the lambda-calculus, like those arising from Böhm trees and from the contextual preorder. Then, we introduce applicative distances capturing higher-order Scott topologies, including reflexive objects like the "D-infinity" model. Finally, we provide a quantitative insight on the well-known connection between the Böhm tree of a lambda-term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.

This is joint work with Valentin Maestracci.

Federico Olimpieri

Università di Bologna

Linearizing Intersection Types

We present an effective translation of Cartesian intersection types (where duplication and erasure of resources are allowed) into linear types (where neither duplication nor erasure is permitted). The construction is based on an appropriate notion of operational semantics, called the collapse reduction. From this, we obtain quantitative information about the normalization of simply typed lambda terms and idempotent intersection types. Semantically, we also obtain a proof-relevant version of Ehrhard's extensional collapse.

Davide Barbarossa

Department of Computer Science University of Bath

An overview on Dialectica as Differentiation

"Dialettica" è il nome di una importante trasformazione logica introdotta da Gödel, alla fine degli anni 50, per ottenere risultati di coerenza relativa di HA rispetto al Sistema T, preso come quadro per i metodi finitari nel senso del programma di Hilbert. Questa ha dato luogo poi, tipicamente nella tradizione tedesca, al "proof mining" di molti importanti risultati di matematica classica. Solo una decina di anni fa è stata invece riformulata (da Pierre-Marie Pédrot) in termini più naturali per la logica informatica, come una trasformazione (tipata o non) di programmi tra linguaggi funzionali all'ordine superiore. Questo ha permesso a Pierre-Marie Pédrot e Marie Kerjan, ancora più recentemente (LICS 2024), di accorgersi che tale trasformazione si comportasse in realtà come una trasformazione differenziale su tali linguaggi, nel senso del lambda-calcolo differenziale. 

In questo intervento, basato su un mio preprint che ho scritto negli ultimi mesi, cercherò di chiarire la relazione tra Dialettica e differenziazione, facendo la scommessa che questa relazione, e la sua ragione, appaia più chiara e, soprattutto, più naturale, esprimendola diversamente dal loro articolo: invece del lambda-calcolo differenziale, userò il quadro delle categorie delle lenti e delle categorie differenziali, lasciandoci guidare dall'intuizione della geometria differenziale.

Giulia Manara

Université Paris Cité & 

Università Roma Tre

Processes as Formulas, Choreographies as Proofs

In this talk, we discuss proof-theoretic methodologies for studying concurrent programs. In particular, we present a new approach inspired by the standard interpretation of logic program execution as proof search. For this purpose, we first recall syntax and semantics of the recursion-free π-calculus and choreographies. Then we introduce the logic PiL, an extension of multiplicative additive linear logic with a non-commutative non-associative connective (to model the prefix-operator), and nominal quantifiers (to model restriction).

We prove cut-elimination for this system, and we establish a correspondence between proofs of formulas encoding processes of π-calculus and computation trees. We use this correspondence to prove the first completeness result for choreographies with respect to (race-free) deadlock-free processes.

This talk is based on joint work with Matteo Acclavio and Fabrizio Montesi.

Raffaele Di Donna

Université Paris Cité & 

Università Roma Tre

On sequentialization in the presence of weakenings

We study the problem of finding natural conditions for the sequentialization of proof-structures in subsystems of multiplicative exponential linear logic with weakenings. In particular, we consider the famous criterion relating connected components and weakenings, which was proposed right away as a correctness criterion for multiplicative linear logic with units for its simplicity. This attempt failed, because that condition is not sufficient for sequentialization. It is nonetheless a necessary condition for a proof-structure to be sequentializable, and a property which is stable under the cut elimination procedure. It is therefore interesting to look for logical systems in which this condition is also sufficient for sequentialization: for such systems it would be, indeed, a correctness criterion. We show some sufficient conditions under which this is the case, and we present some original and interesting fragments of multiplicative exponential linear logic in which such sufficient conditions hold.

Adrien Ragot

Université Sorbonne Paris Nord & Universit`a Degli Studi Roma Tre

Parsing Correctness Criterion for Second Order Multiplicative Linear Logic

e 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.

Ugo Dal Lago

Università di Bologna

On Interaction, Efficiency, and Reversibility

We give an overview of some results we obtained in the last four years about the so-called Interaction Abstract Machine (IAM in the following) and its efficiency in time and space. More specifically, we are interested in checking whether any invariance result in the style of Slot and van Emde Boas is possible for the IAM. Unfortunately, the answer is going to be negative. Still, while the time inefficiency of the IAM is expected, its space inefficiency could be seen as surprising, given, e.g., the well-known results of Schöpp and coauthors on the characterization of logarithmic space computable functions through a construction very closely related to the IAM. We proceed by giving an hint of how much of the aforementioned results hold for the PAM. We conclude the talk by giving some observations about the IAM’s reversibility properties, which can be seen as partially justifying the results above.

Vito Michele Abrusci

Università Roma Tre

Reflections on proof theory, after the contributions made by linear logic.

A little more than ten years after the birth of proof theory with Hilbert (in 1925 Hilbert gave his famous conference "Uber das Unendliche" - "On the infinite"), I will try to expose some of my reflections on the state of this discipline after the great contributions made by the birth and development of linear logic.