Generalized Connectives for Multiplicative Linear Logic

Authors Matteo Acclavio , Roberto Maieli

Thumbnail PDF


  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Matteo Acclavio
  • Samovar, UMR 5157 Télécom SudParis and CNRS, 9 rue Charles Fourier, 91011 Évry, France
Roberto Maieli
  • Mathematics & Physics Department, Roma Tre University, L.go S. L. Murialdo 1, 00146 Rome, Italy

Cite AsGet BibTex

Matteo Acclavio and Roberto Maieli. Generalized Connectives for Multiplicative Linear Logic. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


In this paper we investigate the notion of generalized connective for multiplicative linear logic. We introduce a notion of orthogonality for partitions of a finite set and we study the family of connectives which can be described by two orthogonal sets of partitions. We prove that there is a special class of connectives that can never be decomposed by means of the multiplicative conjunction ⊗ and disjunction ⅋, providing an infinite family of non-decomposable connectives, called Girard connectives. We show that each Girard connective can be naturally described by a type (a set of partitions equal to its double-orthogonal) and its orthogonal type. In addition, one of these two types is the union of the types associated to a family of MLL-formulas in disjunctive normal form, and these formulas only differ for the cyclic permutations of their atoms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Linear Logic
  • Partitions Sets
  • Proof Nets
  • Sequent Calculus


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. V. Michele Abrusci and Roberto Maieli. Proof nets for multiplicative cyclic linear logic and Lambek calculus. Mathematical Structures in Computer Science, 29(6):733–762, 2019. URL:
  2. Jean-Marc Andreoli. Focussing and proof construction. Annals of Pure and Applied Logic, 107(1):131-163, 2001. URL:
  3. Jean-Marc Andreoli and Laurent Mazaré. Concurrent construction of proof-nets. In International Workshop on Computer Science Logic, pages 29-42. Springer, 2003. URL:
  4. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics in multiplicative-additive linear logic. Annals of Pure and Applied Logic, 102(3):247-282, 2000. URL:
  5. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical logic, 28(3):181-203, 1989. URL:
  6. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL:
  7. Jean-Yves Girard. Multiplicatives. Rendiconti del Seminario Matematico, pages 11-34, 1987. Google Scholar
  8. Jean-Yves Girard. On Geometry of Interaction. In Helmut Schwichtenberg, editor, Proof and Computation, pages 145-191, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  9. Jean-Yves Girard. On the meaning of logical rules II: multiplicatives and additives. NATO ASI Series F Computer and Systems Sciences, 175:183-212, 2000. Google Scholar
  10. Roberto Maieli. Construction of Retractile Proof Structures. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi, pages 319-333. Springer International Publishing, 2014. URL:
  11. Roberto Maieli. Non decomposable connectives of linear logic. Annals of Pure and Applied Logic, 170(11):102709, 2019. URL:
  12. Roberto Maieli and Quintijn Puite. Modularity of proof-nets. Archive for Mathematical Logic, 44(2):167-193, 2005. URL:
  13. Dale Miller and Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science, 474:98-116, 2013. Google Scholar
  14. Robin Milner. Communicating and mobile systems: the Pi-calculus. Cambridge university press, 1999. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail