Speakers

1. Davide Barbarossa: È possibile dare una fondazione critica alla matematica?
   In questo talk informale, esporrò alcune considerazioni di carattere filosofico sulla matematica e sulla logica, alla luce dell'avvento dell'informatica in queste discipline. Proverò a rispondere in maniera affermativa alla domanda nel titolo del talk, proponendo di concettualizzare la matematica e le sue questioni fondazionali tramite un approccio trascendentale, nel senso della (prima) critica Kantiana. Questa posizione filosofica necessita, in maniera evidente, di essere modernizzata ; ma una volta fatto ciò, dovrebbe fornire un quadro concettuale soddisfacente alla matematica ed ai suoi aspetti logici ed informatici. In particolare, dovrebbe fungere anche da sintesi compatibile con i principali approcci filosofici alla logica che, focalizzandosi spesso su un solo aspetto, risultano altrimenti incompatibili tra loro.

2. Matteo Acclavio: I don't need no jumps
   In this talk, I will show canonical proof nets for the multiplicative fragment of intuitionistic linear logic (IMLL) equipped with a polynomial-time correctness criterion, proof translation, and sequentialization procedure. I will explain why  in the classical setting (MLL) is impossible under the assumption PTIME ≠ PSPACE, and why such a result is possible in the intuitionistic one. I will present two main results: a correctness criterion showing that jumps are unnecessary in IMLL, and a simple procedure for rewiring jumps in a canonical way.

3. Paolo Pistone: On the Tropical Geometry of Probabilistic Programming Languages (jww Davide Barbarossa)
   In the last few years there has been a growing interest towards methods for statistical inference and learning based on computational geometry and, notably, tropical geometry, that is, the study of algebraic varieties over the min-plus semiring. At the same time, recent work has demonstrated the possibility of interpreting higher-order probabilistic programming languages in the framework of tropical mathematics, by exploiting algebraic and categorical tools coming from the semantics of linear logic. In this work we combine these two worlds, showing that tools and ideas from tropical geometry can be used to perform statistical inference over higher-order probabilistic programs. Notably, we first show that each such program can be associated with a degree and a n-dimensional polyhedron that encode its most likely runs. Then, we use these tools to design an intersection type system that estimates most likely runs in a compositional and efficient way.

4. Adrien Ragot: Asymmetric linear realisability
   Realisability connects computer science and logic by interpreting proofs as computational processes. While logicians view it as a form of semantics, its meaning for computer scientists is often vague. We argue that the most convincing perspective is found in the work of Benton and Hurr (2010), where the adequacy theorem of their realisability model yields a proof of compiler correctness from a high-level language to machine code.
   Realisability for linear logic has been explored by E. Beffara and T. Seiller, but their approaches rely on symmetric interactions. Inspired by the philosophy of Benton and Hurr, we propose a framework for linear realisability that supports asymmetric interactions, mirroring how machines operate with a stack. This allows us to derive an adequacy theorem that directly yields a correct compiler.
   Key to our approach is the introduction of roles, which create symmetry at the type level without requiring the interaction of processes to be symmetric. This makes it possible to lift an oriented pre-semantics of linear logic to a full semantics, ensuring the correctness of the derived compiler.
   We illustrate our method with two examples: a higher-order $\pi$-calculus and a variant of the functional machine calculus. Our approach also has potential for implicit complexity: by restricting to soft linear logic (SLL), it is likely that under reasonable assumptions, the compiler transforms an SLL-proof into a process which
   runs in polynomial time.

5. Stefano Catozi: On Jumps, Interactions and Intersections
   The Jumping Abstract Machine (JAM), introduced by Danos and Regnier as an optimization of the Interaction Abstract Machine (IAM), provides an evaluation mechanism for the λ-calculus. We study a parametric generalization of the JAM and show its correspondence with non-idempotent intersection types: for any normalizing term t, the number of machine steps can be extracted from its type derivation. This correspondence allows us to analyze the machine’s complexity, proving that, for each finite parameter, its running time is polynomial in the number of β-steps, making it a reasonable model of computation.

6. Francesco Dagnino: Quantitative equality in graded linear logic
   
   Equality in predicate First-Order Logic (FOL) is fairly well understood. From a syntactic point of view, it can be characterized as a binary predicate that is reflexive and substitutive, and from a categorical perspective, it can be described in terms of left adjoints. This approach can be easily rephrased in the context of predicate Linear Logic (LL); however, this smooth translation has an unexpected consequence: equality can be used an arbitrary number of times. This is not desirable in a linear setting where the goal is to control the use of resources. Moreover, it does not allow a quantitative interpretation of equality, for instance, as a distance, which limits the use of Linear Logic as a foundation for quantitative reasoning.
   
   In this talk, we explore a novel approach to equality in predicate Linear Logic with graded modalities, which allow us to control its use by explicitly modeling resources, thus enabling its quantitative interpretation as a distance. We present a calculus for (fragments of) such a logic, together with a sound and complete categorical semantics using Lawvere's hyperdoctrines, encompassing models in metric spaces with Lipschitz maps and quantitative realizability. If time permits, we will discuss directions for further developments, including a refinement of the calculus and its connection with quantitative equational theories.
   
   This is joint work with Fabio Pasquali.
   
   

7. Gabriele Vanoni: A Call-by-Value Geometry of Interaction, Finally?

In the first part of the talk, I will try to sketch the history of the attempts to devise a Geometry of Interaction for call-by-value evaluation. In the second part, I will sketch at least one new solution to this problem, arguably more canonical than all the previous attempts and rooted in the proof theory of (classical) linear logic.

8. Federico Olimpieri: The lambda calculus, algebraically
   
   We will explore a recent perspective on the theory of lambda calculus, primarily due to Hyland. We will advocate for the concepts of abstract clones and Cartesian operads as a suitable framework for an algebraic definition of lambda calculus. Additionally, we will examine how this definition relates to the standard denotational semantics notion of a reflexive object in a Cartesian closed category. Finally, we will conclude by discussing potential extensions of this framework to the rewriting theory of lambda terms.

9. Raffaele Di Donna: Connectivity and (intuitionistic) Linear Logic

We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic (MELL) to recover a sequent calculus proof from a proof-structure. We present a geometric condition on untyped proof-structures allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of MELL for which this property is indeed a correctness criterion. In a suitable fragment of multiplicative linear logic with units, the criterion yields a characterization of the equivalence induced by permutations of rules in sequent calculus. Finally, in intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and it is sufficient for sequentialization in the axiom-free setting.