ABSTRACT. 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 par-vertex, on a splitting tensor-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) - similar results from the literature required more involved encodings.

ABSTRACT. In linear logic, a connective's right-introduction rule is invertible if and only if its left-introduction rule is not. This fact suggests the following notion of polarity: a connective is negative if its right-introduction rule is invertible and positive otherwise. Negation inverts polarity. A two-sided sequent calculus for first-order linear logic with only negative connectives has an appealing proof theory. Proof search proceeds by alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules, corresponding to goal-reduction and backchaining, respectively. These phases are formalized by multifocused proofs, which illuminate differences between proofs in intuitionistic and linear logic. We decompose linear logic into three sublogics: L0 (first-order intuitionistic logic with conjunction, implication, and universal quantification); L1 (extending L0 with linear implication, retaining its intuitionistic character); and L2 (containing multiplicative falsity, encompassing classical linear logic). Notably, the single-conclusion restriction on sequents does not need to be imposed (as Gentzen did) to define intuitionistic logic proofs since it arises as a feature of multifocused proofs of L0 and L1 sequents. While multifocused proofs of L2 sequents can contain parallel applications of left-introduction rules, proofs of L0 and L1 sequents cannot exploit such parallel rule application. This notion of parallelism in proofs facilitates a novel treatment of disjunctions and existential quantifiers in natural deduction for intuitionistic logic. The cut-elimination theorem for the focused proof system is proved in the appendix.

ABSTRACT. 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 $\lambda$-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.

ABSTRACT. Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call ‘memory trees’. The memory tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches.

We develop the associated theories of program approximation: the first approach—more classic—is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its memory tree. As a corollary, we obtain that the equality induced by memory trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.

ABSTRACT. Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped lambda calculus and serve as the basis for many notions of computability, such as realizability theory. But PCAs support a very limited notion of computation by only incorporating non-termination as a computational effect. To provide a framework that better internalizes a wide range of computational effects, this paper puts forward the notion of Monadic Combinatory Algebras (MCAs). MCAs generalize the notion of PCAs by structuring the combinatory algebra over an underlying computational effect, embodied by a monad. We show that MCAs can support various side effects through the underlying monad, such as non-determinism, stateful computation and continuations. We further obtain a categorical characterization of MCAs within Freyd Categories, following a similar connection for PCAs. Moreover, we explore the application of MCAs in realizability theory, presenting constructions of effectful realizability triposes and assemblies derived through evidenced frames, thereby generalizing traditional PCA-based realizability semantics. The monadic generalization of the foundational notion of PCAs provides a comprehensive and powerful framework for internally reasoning about effectful computations, paving the path to a more encompassing study of computation and its relationship with realizability models and programming languages.

ABSTRACT. The notion of categorical model of linear logic is now well studied and established around the notion of linear-non-linear adjunction, which encompasses the previous notions of Seely categories, Lafont categories and linear categories. These categorical structures have counterparts in the realm of ∞-categories, which can thus be thought of as weak forms of models of linear logic. The goal of this article is to formally introduce them and study their relationships. We show that ∞-linear-non-linear adjunctions still play the role of a unifying notion of model in this setting. Moreover, we provide a sufficient condition for a symmetric monoidal ∞-category to be Lafont. Finally, we illustrate our constructions by providing models: we construct linear-non-linear adjunctions which generalize well-known models in relations (and variants based on profunctors or spans), domains and vector spaces. In particular, we introduce a model based on spectra, a homotopical variant of abelian groups.

ABSTRACT. Constructing solutions to recursive domain equations is a well-known, important problem in the study of programs and programming languages. Mathematically speaking, the problem is finding a fixed point (up to isomorphism) of a suitable functor over a suitable category. A particularly useful instance, inspired by the step-indexing technique, is where the functor is over (a subcategory of) the category of presheaves over the ordinal ω and the functors are locally-contractive, also known as guarded functors. This corresponds to step-indexing over natural numbers. However, for certain problems, e.g., when dealing with infinite non-determinism, one needs to employ trans-finite step-indexing, i.e., consider presheaf categories over higher ordinals. Prior work on trans-finite step-indexing either only considers a very narrow class of functors over a particularly restricted subcategory of presheaves over higher ordinals, or treats the problem very generally working with sheaves over an arbitrary complete Heyting algebras with a well-founded basis.

In this paper we present a solution to the guarded domain equations problem over all guarded functors over the category of presheaves over ordinal numbers, as well as its mechanization in the Rocq proof assistant. As the categories of sheaves and presheaves over ordinals are equivalent, our main contribution is simplifying prior work from the setting of the category of sheaves to the setting of the category of presheaves and mechanizing it — presheaves are more amenable to mechanization in a proof assistant.

ABSTRACT. After Craig’s seminal results on interpolation theorem, a number and variety of proof-techniques, be they semantical or proof-theoretical, have been designed to establish interpolation theorems. Among them, Maehara’s method stand at a specific place due to its applicability to a wide range of logics that admit cut-free complete proof systems.

By reconsidering Maehara's method, this paper shows how one can extract a “proof-relevant” interpolation theorem for first-order linear-logic. The result can be stated as follows: if π is a cut-free proof of A⊢B, we can find (i) a formula C in the common vocabulary of A and B and (ii) proofs π1 of A⊢C and π2 of C⊢B such that the proof π' of A⊢B, obtained by cutting π1 with π2 on C, normalizes to π by cut-reduction. This investigation of proof-relevant interpolation is carried out in two frameworks.

First, in the traditional sequent calculus, we show that interpolation can be organized in two phases: (i) a bottom-up phase which decorates the sequents with a so-called splitting followed by (ii) a top-down phase which solves the interpolation problem, synthesizing the interpolant by introducing cuts. The flexibility of the approach is exploited to carry the interpolation-as-cut-introduction from linear logic to classical and intuitionistic logics, in such a way to satisfy not only Craig's constraints on the vocabulary of the interpolant but Lyndon's as well as.

Second, we move to the framework of System L, also known as Curien & Herbelin's duality of computation, and prove a computational version of the above result in System L. This results unveils, the computational content of Maheara's interpolation method which can therefore be understood as the factorization of any computation into (i) a term and (ii) an evaluation context which interact through an interface type provided by the interpolant, satisfying the usual constraints.

Finally, we discuss how the result relates to a proof-relevant refinement of Prawitz' proof of the interpolation theorem in natural deduction investigated by Čubrić in the 90’s for the simply typed λ-calculus, while allowing its generalization to a variety of logics and computational frameworks that we discuss as ongoing and future works.

ABSTRACT. Classical logic can be embedded into intuitionistic logic by inserting double negations in formulas. Several translations generalize this idea by using monad operators instead of double negations. They eliminate particular axioms, for instance the principle of excluded middle or the principle of explosion, and therefore can be used to embed classical logic into intuitionistic logic or intuitionistic logic into minimal logic. Such translations have been defined for first-order logic.

In this paper, we define a translation, parameterized by monad operators, for higher-order logic. In particular, the property that any formula and its translation are equivalent in the presence of the eliminated axiom holds under functional extensionality and propositional extensionality. We apply this translation to embed higher-order classical (respectively intuitionistic) logic into higher-order intuitionistic (respectively minimal) logic. By adapting Friedman's trick, we identify fragments of higher-order logic for which we can actually constructivize the proofs without modifying the proven statements.