Publications

2025

1. 

   Functorial Models of Differential Linear Logic

   Marie Kerjean, Valentin Maestracci, and Morgan Rogers

   In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), 2025

   ISSN: 1868-8969

   Abs DOI PDF

   Differentiation in logic has several sources of inspiration. The most recent is differentiable programming, models of which demand functoriality and good typing properties. More historical is reverse denotational semantics, taking inspiration from models of Linear Logic to differentiate proofs and λ-terms. In this paper, we take advantage of the rich structure of categorical models of Linear Logic to give a new functorial presentation of differentiation. We define differentiation as a functor from a coslice of the category of smooth maps to the category of linear maps. Extending linear–non-linear adjunction models of Linear Logic, this produces models of Differential Linear Logic. We use these functorial presentations to shed new light on integration in differential categories.

2. 

   The Lambda Calculus Is Quantifiable

   Valentin Maestracci and Paolo Pistone

   In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025), 2025

   ISSN: 1868-8969

   Abs DOI PDF

   In this paper we introduce several 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 \λ\-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_}infty model. Finally, we provide a quantitative insight on the well-known connection between the Böhm tree of a \λ\-term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.

2020

1. Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory

   Bruno Barras and Valentin Maestracci

   In LFMPT 2020 - Logical Frameworks and Meta-Languages: Theory and Practice 2020, Jun 2020

   Abs

   In this paper, we make a substantial step towards an encoding of Cubical Type Theory (CTT) in the Dedukti logical framework. Type-checking CTT expressions features a decision procedure in a de Morgan algebra that so far could not be expressed by the rewrite rules of Dedukti. As an alternative, 2 Layer Type Theories are variants of Martin-Lf Type Theory where all or part of the definitionalequality can be represented in terms of a so-called external equality. We propose to split the encodingby giving an encoding of 2 Layer Type Theories (2LTT) in Dedukti, and a partial encoding of CTTin 2LTT.

1. 

   From Geometry to Interaction

   Valentin Maestracci and Thomas Seiller

   Abs PDF

   Linear Realisability is a program of research in the line of Geometry of Interaction, where models of computations are used to create models of Linear Logic. This work aims to solve some of the problems of the underlying computational models, and more precisely related to their representation of program execution, by realising them as directed topological spaces. This construction formally shows the decomposition into three parts of the dynamics of computing normal forms: glueing, saturation, hiding. Gluing composes programs without loss of information, saturation computes the information represented by the space, and finally hiding removes partial computations. This shows that execution transforms coSpans/Pushouts –purely geometric information with implicit computational content –, into Spans/Pullbacks – explicit functional/relational information, or a normal form. Finally, it explains the so-called 2-cocycle (or trefoil ) property [32] of interaction graphs as a reflection of geometric associativity. All of this opens the link with directed algebraic topology and glueing as a potential way to creates new models of Linear Realisability.

2025

1. 

   Un petit pas vers une Logique Open Source

   Valentin Maestracci

   2025

   PDF