5 citations
- École PolytechniqueFR5 papers
- Laboratoire d'Informatique de l'École PolytechniqueFR5 papers
- Institut national de recherche en sciences et technologies du numériqueFR4 papers
- Centre National de la Recherche ScientifiqueFR2 papers
- Institut de Recherche en Informatique FondamentaleFR2 papers
- Université Paris CitéFR2 papers
- École Normale Supérieure d'AbidjanCI1 paper
- École Normale Supérieure de LyonFR1 paper
- Laboratoire de l'Informatique du ParallélismeFR1 paper
- OLAS: Fondements opérationnels, logiques et algébriques des systèmes logicielsIT1 paper
- PICUBE: Les assistants à la démonstration au cœur du raisonnement mathématiqueFR1 paper
- Sorbonne Paris CitéFR1 paper
6 papers
Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem
Paul-André Melliès, Noam Zeilberger
We begin by explaining how any context-free grammar encodes a functor of operads from a freely generated operad into a certain "operad of spliced words". This motivates a more gene…
A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
Lê Thành Dũng Nguyên, Lutz Straßburger
Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originate…
Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
Beniamino Accattoli
This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials…
Reasonable Space for the -Calculus, Logarithmically
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
Can the -calculus be considered a reasonable computational model? Can we use it for measuring the time space consumption of algorithms? While the literature conta…
Combinatorial Proofs and Decomposition Theorems for First-order Logic
Dominic Hughes, Lutz Straßburger, Jui-Hsuan Wu
We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof sy…
An Analytic Propositional Proof System on Graphs
Matteo Acclavio, Ross Horne, Lutz Straßburger
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-co…