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 proofs 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 the first author 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 our recent work on the proof theory of the modal μ-calculus.

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 Čubrić in the simply-typed λ-calculus with sums and more recently in linear, classical and intuitionistic sequent calculi. We give a new proof of Čubrić’s proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in Rocq.

Abstract 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, $$\mu \textsf {LL}_{\Box }^{\infty }$$ μ LL □ ∞ , 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 $$\mu \textsf {LL}_{\Box }^{\infty }$$ μ LL □ ∞ 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.

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 "Ohana trees". The Ohana 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 Ohana tree. As a corollary, we obtain that the equality induced by Ohana 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.

This paper investigates the denotational invariants of non-wellfounded and circular proofs of linear logic with least and greatest fixed points, μLL, by providing a categorical semantics. More precisely the paper successively introduces semantics for (i) non-wellfounded pre-proofs, be they valid or not, (ii) valid pre-proofs exploiting their validity condition by considering an orthogonality construction on the given categorical model and finally (iii) circular strongly valid pre-proofs, exploiting both validity and regularity in order to define inductively the interpretation. Then the paper investigates the semantical content of the translation from finitary proofs to non-wellfounded proofs and, conversely, from (strongly valid) circular proofs to finitary proofs, showing that both translations preserve the interpretation.

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 $μ$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 $μ$MALL validity criterion and how the language simulates the cut-elimination procedure of $μ$MALL.

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 μ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 μMALL validity criterion and how the language simulates the cut-elimination procedure of μMALL.

Extensions of Girard’s linear logic by least and greatest fixed point operators (μMALL) have been an active field of research for almost two decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this paper, we compare the relative expressivity, at the level of provability, of two complementary infinitary proof systems: finitely branching non-wellfounded proofs (μMALL^∞) vs. infinitely branching well-founded proofs (μMALL_{ω,∞}). Our main result is that μMALL^∞ is strictly contained in μMALL_{ω,∞}. For inclusion, we devise a novel technique involving infinitary rewriting of non-wellfounded proofs that yields a wellfounded proof in the limit. For strictness of the inclusion, we improve previously known lower bounds on μMALL^∞ provability from Π⁰₁-hard to Σ¹₁-hard, by encoding a sort of Büchi condition for Minsky machines.

Abstract This paper establishes cut-elimination for $$\mathsf {\mu LL^\infty }$$ , $$\mathsf {\mu LK^\infty }$$ and $$\mathsf {\mu LJ^\infty }$$ , that are non-wellfounded sequent calculi with least and greatest fixed-points, by expanding on prior works by Santocanale and Fortier [20] as well as Baelde et al. [3, 4]. The paper studies a fixed-point encoding of $$\textsf{LL}$$ exponentials in order to deduce those cut-elimination results from that of $$\mathsf {\mu MALL^\infty }$$ . Cut-elimination for $$\mathsf {\mu LK^\infty }$$ and $$\mathsf {\mu LJ^\infty }$$ is obtained by developing appropriate linear decorations for those logics.

Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting "infinitary" behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (μMALL), in particular, recent systems based on "circular" and "non-wellfounded" reasoning. In this paper, we show that μMALL is undecidable. More explicitly, we show that the general non-wellfounded system is Π⁰₁-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Σ⁰₁). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Σ⁰₁-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Σ⁰₁-complete.

The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formulas rather than the contents of their proofs (or refutations). Linear logic equipped with the least and greatest fixpoint operators (μMALL) has been an active field of research for the past one and a half decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this paper, we extend the phase semantics of multiplicative additive linear logic (a.k.a. MALL) to μMALL with explicit (co)induction (i.e. μMALL^{ind}). We introduce a Tait-style system for μMALL called μMALL_ω where proofs are wellfounded but potentially infinitely branching. We study its phase semantics and prove that it does not have the finite model property.

International audience

Non-wellfounded and circular proofs have been recognised over the past decade as a valuable tool to study logics expressing (co)inductive properties, e.g. μ-calculi. Such proofs are non-wellfounded sequent derivations together with a global validity condition expressed in terms of progressing threads. While the cut-free fragment of circular proofs is satisfactory, cuts are poorly treated and the non-canonicity of sequent proofs becomes a major issue in the non-wellfounded setting. The present paper develops for (multiplicative linear logic with fixed points) the theory of infinets – proof-nets for non-wellfounded proofs. Our structures handles infinitely many cuts therefore solving a crucial shortcoming of the previous work [19]. We characterise correctness, define a more complete cut-reduction system and proving a cut-elimination theorem. To that end, we also provide an alternate cut reduction for non-wellfounded sequent calculus.

Abstract The ${\lambda }$-calculus enjoys the property that each ${\lambda }$-term has at least one fixed point, which is due to the existence of a fixed point combinator. It is unknown whether it enjoys the ‘fixed point property’ stating that each ${\lambda }$-term has either one or infinitely many pairwise distinct fixed points. We show that the fixed point property holds when considering possibly open fixed points. The problem of counting fixed points in the closed setting remains open, but we provide sufficient conditions for a ${\lambda }$-term to have either one or infinitely many fixed points. In the main result of this paper we prove that in every sensible ${\lambda }$-theory there exists a ${\lambda }$-term that violates the fixed point property. We then study the open problem concerning the existence of a double fixed point combinator and propose a proof technique that could lead towards a negative solution. We consider interpretations of the ${\lambda } {\mathtt{Y}}$-calculus into the ${\lambda }$-calculus together with two reduction extension properties, whose validity would entail the non-existence of any double fixed point combinators. We conjecture that both properties hold when typed ${\lambda } {\mathtt{Y}}$-terms are interpreted by arbitrary fixed point combinators. We prove reduction extension property I for a large class of fixed point combinators. Finally, we prove that the ${\lambda }{\mathtt{Y}}$-theory generated by the equation characterizing double fixed point combinators is a conservative extension of the ${\lambda }$-calculus.

The genesis of this special issue was in a meeting that took place at Université Paris Diderot on December 15 and 16, 2016. Dale Miller, Professor at École polytechnique, had turned 60 a few days earlier. In a career spanning over three decades and in work conducted in collaboration with several students and colleagues, Dale had had a significant influence in an area that can be described as structural proof theory and its application to computation and reasoning. In recognition of this fact, several of his collaborators thought it appropriate to celebrate the occasion by organizing a symposium on topics broadly connected to his areas of interest and achievements. The meeting was a success in several senses: it was attended by over 35 people, there were 15 technical presentations describing new results, and, quite gratifyingly, we managed to spring the event as a complete surprise to Dale.

Circular (ie. non-wellfounded but regular) proofs have received increasing interest in recent years with the simultaneous development of their applications and meta-theory: infinitary proof theory is now well-established in several proof-theoretical frameworks such as Martin Löf's inductive predicates, linear logic with fixed points, etc. In the setting of non-wellfounded proofs, a validity criterion is necessary to distinguish, among all infinite derivation trees (aka. pre-proofs), those which are logically valid proofs. A standard approach is to consider a pre-proof to be valid if every infinite branch is supported by an infinitely progressing thread. The paper focuses on circular proofs for MALL with fixed points. Among all representations of valid circular proofs, a new fragment is described, based on a stronger validity criterion. This new criterion is based on a labelling of formulas and proofs, whose validity is purely local. This allows this fragment to be easily handled, while being expressive enough to still contain all circular embeddings of Baelde's muMALL finite proofs with (co)inductive invariants: in particular deciding validity and computing a certifying labelling can be done efficiently. Moreover the Brotherston-Simpson conjecture holds for this fragment: every labelled representation of a circular proof in the fragment is translated into a standard finitary proof. Finally we explore how to extend these results to a bigger fragment, by relaxing the labelling discipline while retaining (i) the ability to locally certify the validity and (ii) to some extent, the ability to finitize circular proofs.

Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier; the second one has never been studied in infinitary systems. In this paper, we consider the infinitary proof system muMALLi for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish muMALLi as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.

Modal μ-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-theoretical side. Nevertheless, axiomatizations have been given for both linear and branching time μ-calculi, with quite involved completeness arguments. We come back to this central problem, considering it from a proof search viewpoint, and provide some new completeness arguments in the linear time μ-calculus. Our results only deal with restricted classes of formulas that closely correspond to (non-alternating) ω-automata but, compared to earlier proofs, our completeness arguments are direct and constructive. We first consider a natural circular proof system based on sequent calculus, and show that it is complete for inclusions of parity automata expressed as formulas, making use of Safra's construction directly in proof search. We then consider the corresponding finitary proof system, featuring (co)induction rules, and provide a partial translation result from circular to finitary proofs. This yields completeness of the finitary proof system for inclusions of sufficiently deterministic parity automata, and finally for arbitrary Büchi automata.

Various logics have been introduced in order to reason over (co)inductive specifications and, through the Curry-Howard correspondence, to study computation over inductive and coinductive data. The logic mu-MALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators. In this paper, we investigate the semantics of mu-MALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data. We provide mu-MALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of "essentially finite designs", which are those designs performing a finite computation followed by a copycat. On the way to completeness, we investigate semantic inclusion, proving its decidability (given two formulas, we can decide whether the semantics of one is included in the other's) and completeness (if semantic inclusion holds, the corresponding implication is provable in mu-MALL).

Λμ-calculus is a Böhm-complete extension of Parigot's Λμ-calculus closely related with delimited control in functional programming. In this article, we investigate the meta-theory of untyped Λμ-calculus by proving confluence of the calculus and characterizing the basic observables for the Separation theorem, canonical normal forms . Then, we define Λ s , a new type system for Λμ-calculus that contains a special type construction for streams, and prove that strong normalization and type preservation hold. Thanks to the new typing discipline of Λ s , new computational behaviors can be observed, which were forbidden in previous type systems for λμ-calculi. Those new typed computational behaviors witness the stream interpretation of Λμ-calculus.

The /spl lambda//spl mu/-calculus is an extension of the /spl lambda/-calculus introduced in 1992 by Parigot (M. Parigot, 1992) in order to generalize the Curry-Howard isomorphism to classical logic. Two versions of the calculus are usually considered in the literature: Parigot's original syntax and an alternative syntax introduced by de Groote. In 2001, David and Py (R. David, 2001) proved that the Separation Property (also referred to as Bohm theorem) fails for Parigot's /spl lambda//spl mu/-calculus. By analyzing David & Py's result, we exhibit an extension of Parigot's /spl lambda//spl mu/-calculus, the /spl Lambda//spl mu/-calculus, for which the Separation Property holds and which is built as an intermediate language between Parigot's and de Groote's /spl lambda//spl mu/-calculi. We prove the theorem and describe how /spl Lambda//spl mu/-calculus can be considered as a calculus of terms and streams. We then illustrate Separation in showing how in /spl Lambda//spl mu/-calculus it is possible to separate the counter-example used by David & Py.