arXiv subjects

Alexis Saurin

Publications and source records attributed to Alexis Saurin.

11 recordsLinked to original sources

arXiv2026

Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-\v{C}ubri\'c Interpolation

Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follow a method first introduced by Maehara for the Sequent Calculus and then adapted by Prawitz to Natural Deduction. The result can be strengthened to a proof-relevant version, taking proof terms into account: this was first established by \v{C}ubri\'c in the simply-typed lambda-calculus with sums and more recently in linear, classical and intuitionistic sequent calculi. We give a new proof of \v{C}ubri\'c's proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in Rocq.

cs.LO↗

arXiv2025

Proceedings Twelfth Workshop on Fixed Points in Computer Science

This EPTCS volume contains the post-proceedings of the Twelfth International Workshop on Fixed Points in Computer Science, presenting a selection of the works presented during the workshop that took place in Naples (Italy) on the 19th and 20th of February 2024 as a satellite of the International Conference on Computer Science Logic (CSL 2024).

cs.LO↗

arXiv2025

Compression for Coinductive Rewriting and the Cut-Elimination of Non-Wellfounded Proofs

We introduce a generic presentation of "syntactic objects built by mixed induction and coinduction" encompassing all standard kinds of infinitary terms, as well as derivation trees in non-wellfounded proof systems. We then define a coinductive notion of infinitary rewriting of such objects, which is equivalent to the original presentation of infinitary rewriting relying on metric convergence and ordinal-indexed sequences of rewriting steps. This provides a unified coinductive presentation of e.g. first-order infinitary rewriting, infinitary {\lambda}-calculi, and cut-elimination in non-wellfounded proofs. We then formulate and study the coinductive counterpart of compression, i.e. the property of an infinitary rewriting system such that all rewriting sequences of any ordinal length can be "compressed" to equivalent sequences of length at most \omega (which ensures that they can be finitely approximated). We characterise compression in our generic setting for coinductive rewriting, "factorising" the part of the proof that can be performed at this level of generality. Our proof is fully coinductive, avoiding any detour via rewriting sequences. Finally we focus on the non-wellfounded proof system \muMALL\infty for multiplicative-additive linear logic with fixed points, and we put our results to work in order to prove that compression holds for cut-elimination in this setting, which is a key lemma of several extensions of cut-elimination to similar systems.

cs.LO↗

arXiv2025

A uniform cut-elimination theorem for linear logics with fixed points and super exponentials

In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proof of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives. Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination. More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller's subexponentials and from Bauer and Laurent's super exponentials. Our work is motivated on the one hand by Baillot's work on light logics with recursive types and on the other hand by Bauer and Saurin's recent work on the proof theory of the modal {\mu}-calculus.

cs.LO↗

arXiv2025

On the cut-elimination of the modal $\mu$-calculus: Linear Logic to the rescue

This paper presents a proof-theoretic analysis of the modal $\mu$-calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal $\mu$-calculus, using methods from linear logic and its exponential modalities. To achieve this, we introduce a new system, \muLLmodinf{}, which is a linear version of the modal $\mu$-calculus, intertwining the modalities from the modal $\mu$-calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i) proving cut-elimination for \muLLmodinf{} and (ii) translating proofs of the modal mu-calculus into this new system via a ``linear translation'', allowing us to extract the cut-elimination result.

cs.LO↗

arXiv2025

Ohana trees, linear approximation and multi-types for the $\lambda$I-calculus: No variable gets left behind or forgotten!

Although the $\lambda$I-calculus is a natural fragment of the $\lambda$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable $\lambda$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $\lambda$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $\lambda$I-term is an annotated version of its B\"ohm 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 $\lambda$I-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the $\lambda$-calculus, which is known to yield proper models of the $\lambda$I-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, (...)

cs.LO↗

arXiv2023

The exponential logic of sequentialization

Linear logic has provided new perspectives on proof-theory, denotational semantics and the study of programming languages. One of its main successes are proof-nets, canonical representations of proofs that lie at the intersection between logic and graph theory. In the case of the minimalist proof-system of multiplicative linear logic without units (MLL), these two aspects are completely fused: proof-nets for this system are graphs satisfying a correctness criterion that can be fully expressed in the language of graphs. For more expressive logical systems (containing logical constants, quantifiers and exponential modalities), this is not completely the case. The purely graphical approach of proof-nets deprives them of any sequential structure that is crucial to represent the order in which arguments are presented, which is necessary for these extensions. Rebuilding this order of presentation - sequentializing the graph - is thus a requirement for a graph to be logical. Presentations and study of the artifacts ensuring that sequentialization can be done, such as boxes or jumps, are an integral part of researches on linear logic. Jumps, extensively studied by Faggian and di Giamberardino, can express intermediate degrees of sequentialization between a sequent calculus proof and a fully desequentialized proof-net. We propose to analyze the logical strength of jumps by internalizing them in an extention of MLL where axioms on a specific formula, the jumping formula, introduce constrains on the possible sequentializations. The jumping formula needs to be treated non-linearly, which we do either axiomatically, or by embedding it in a very controlled fragment of multiplicative-exponential linear logic, uncovering the exponential logic of sequentialization.

cs.LO↗

arXiv2023

A Curry-Howard Correspondence for Linear, Reversible Computation

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic $\mu$MALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy $\mu$MALL validity criterion and how the language simulates the cut-elimination procedure of $\mu$MALL.

cs.LO↗

arXiv2020

Bouncing threads for infinitary and circular proofs

We generalize the validity criterion for the infinitary proof system of the multiplicative additive linear logic with fixed points. Our criterion is designed to take into account axioms and cuts. We show that it is sound and enjoys the cut elimination property. We finally study its decidability properties, and prove that it is undecidable in general but becomes decidable under some restrictions.

cs.LO↗

arXiv2013

Proceedings First Workshop on Control Operators and their Semantics

The focus of the papers presented in this volume is on the interplay between syntax and semantics in case of languages, namely the central question of what a program means and how it does define the intended procedure. This is a crucial issue especially in the case of control operators, since they are as powerful as potentially obscure, and programs that use them are usually more error-prone than purely declarative ones. The included contributions provide perspectives on the topic of control operators via operational semantics of formal calculi as well as type assignment systems, denotational semantics, game semantics, category theory and logic.

cs.LO↗

arXiv2011

Intersection Logic in sequent calculus style

The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not standard. Between all the logics that have been proposed as its foundation, we consider ISL, which gives a logical interpretation of the intersection by splitting the intuitionistic conjunction into two connectives, with a local and global behaviour respectively, being the intersection the local one. We think ISL is a logic interesting by itself, and in order to support this claim we give a sequent calculus formulation of it, and we prove that it enjoys the cut elimination property.

cs.LO↗