6 Search Results for "Guglielmi, Alessio"

Document
DOI: 10.4230/LIPIcs.FSCD.2025.29
Linear Logic Using Negative Connectives

Authors: Dale Miller

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
In linear logic, the invertibility of a connective’s right-introduction rule is equivalent to the non-invertibility of its left-introduction rule. This duality motivates the concept of polarity: a connective is termed negative if its right-introduction rule is invertible, and positive otherwise. A two-sided sequent calculus for first-order linear logic featuring only negative connectives exhibits a compelling proof theory. Proof search in such a system unfolds through alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules, mirroring the processes of goal-reduction and backchaining, respectively. These phases are formalized here using the framework of multifocused proofs. We analyze linear logic by dissecting it into three sublogics: L₀ (first-order intuitionistic logic with conjunction, implication, and universal quantification); L₁ (an extension of L₀ incorporating linear implication which preserves its intuitionistic nature); and L₂ (which includes multiplicative falsity ⊥ and encompasses classical linear logic). It is worth noting that the single-conclusion restriction on sequents, a constraint imposed by Gentzen, is not a prerequisite for defining intuitionistic logic proofs within this framework, as it emerges naturally by restricting the formulas to those of L₀ and L₁. While multifocused proofs of L₂ sequents can accommodate parallel applications of left-introduction rules, proofs of L₀ and L₁ sequents cannot leverage such parallel rule applications. This notion of parallelism within proofs enables a novel approach to handling disjunctions and existential quantifiers in the natural deduction system for intuitionistic logic.
Cite as

Dale Miller. Linear Logic Using Negative Connectives. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{miller:LIPIcs.FSCD.2025.29,
  author =	{Miller, Dale},
  title =	{{Linear Logic Using Negative Connectives}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{29:1--29:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.29},
  URN =		{urn:nbn:de:0030-drops-236442},
  doi =		{10.4230/LIPIcs.FSCD.2025.29},
  annote =	{Keywords: Linear logic, multifocused proofs, sequent calculus}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.24
Fair Termination of Asynchronous Binary Sessions

Authors: Luca Padovani and Gianluigi Zavattaro

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
Cite as

Luca Padovani and Gianluigi Zavattaro. Fair Termination of Asynchronous Binary Sessions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{padovani_et_al:LIPIcs.ECOOP.2025.24,
  author =	{Padovani, Luca and Zavattaro, Gianluigi},
  title =	{{Fair Termination of Asynchronous Binary Sessions}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{24:1--24:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.24},
  URN =		{urn:nbn:de:0030-drops-233169},
  doi =		{10.4230/LIPIcs.ECOOP.2025.24},
  annote =	{Keywords: Binary sessions, fair asynchronous subtyping, fair termination, linear logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.39
A Strictly Linear Subatomic Proof System

Authors: Victoria Barrett, Alessio Guglielmi, and Benjamin Ralph

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We present a subatomic deep-inference proof system for a conservative extension of propositional classical logic with decision trees that is strictly linear. In a strictly linear subatomic system, a single linear rule shape subsumes not only the structural rules, such as contraction and weakening, but also the unit equality rules. An interpretation map from subatomic logic to propositional classical logic recovers the usual semantics and proof theoretic properties. By using explicit substitutions that indicate the substitution of one derivation into another, we are able to show that the unit-equality inference steps can be eliminated from a subatomic system for propositional classical logic with only a polynomial complexity cost in the size of the derivation, from which it follows that the system p-simulates Frege systems, and we show cut elimination for the resulting strictly linear system.
Cite as

Victoria Barrett, Alessio Guglielmi, and Benjamin Ralph. A Strictly Linear Subatomic Proof System. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 39:1-39:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{barrett_et_al:LIPIcs.CSL.2025.39,
  author =	{Barrett, Victoria and Guglielmi, Alessio and Ralph, Benjamin},
  title =	{{A Strictly Linear Subatomic Proof System}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{39:1--39:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.39},
  URN =		{urn:nbn:de:0030-drops-227967},
  doi =		{10.4230/LIPIcs.CSL.2025.39},
  annote =	{Keywords: Deep inference, Open deduction, Subatomic logic, Decision trees, Explicit substitutions, Cut elimination, Proof theory}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.80
Higher-Order Causal Theories Are Models of BV-Logic

Authors: Will Simmons and Aleks Kissinger

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
The Caus[-] construction takes a compact closed category of basic processes and yields a *-autonomous category of higher-order processes obeying certain signalling/causality constraints, as dictated by the type system in the resulting category. This paper looks at instances where the base category C satisfies additional properties yielding an affine-linear structure on Caus[𝒞] and a substantially richer internal logic. While the original construction only gave multiplicative linear logic, here we additionally obtain additives and a non-commutative, self-dual sequential product yielding a model of Guglielmi’s BV logic. Furthermore, we obtain a natural interpretation for the sequential product as "A can signal to B, but not vice-versa", which sits as expected between the non-signalling tensor and the fully-signalling (i.e. unconstrained) par. Fixing matrices of positive numbers for 𝒞 recovers the BV category structure of probabilistic coherence spaces identified by Blute, Panangaden, and Slavnov, restricted to normalised maps. On the other hand, fixing the category of completely positive maps gives an entirely new model of BV consisting of higher order quantum channels, encompassing recent work in the study of quantum and indefinite causal structures.
Cite as

Will Simmons and Aleks Kissinger. Higher-Order Causal Theories Are Models of BV-Logic. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 80:1-80:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{simmons_et_al:LIPIcs.MFCS.2022.80,
  author =	{Simmons, Will and Kissinger, Aleks},
  title =	{{Higher-Order Causal Theories Are Models of BV-Logic}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{80:1--80:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.80},
  URN =		{urn:nbn:de:0030-drops-168789},
  doi =		{10.4230/LIPIcs.MFCS.2022.80},
  annote =	{Keywords: Causality, linear logic, categorical logic, probabilistic coherence spaces, quantum channels}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.9
Removing Cycles from Proofs

Authors: Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
If we track atom occurrences in classical propositional proofs in deep inference, we see that they can form cyclic structures between cuts and identity steps. These cycles are an obstacle to a very natural form of normalisation, that simply unfolds all the contractions in a proof. This mechanism, which we call ‘decomposition’, has many points of contact with explicit substitutions in lambda calculi. In the presence of cycles, decomposition does not terminate, and this is an obvious drawback if we want to interpret proofs computationally. One way of eliminating cycles is eliminating cuts. However, we could ask ourselves whether it is possible to eliminate cycles independently of (general) cut elimination. This paper shows an efficient way to do so, therefore establishing the independence of decomposition from cut elimination. In other words, cut elimination in propositional logic can be separated into three separate procedures: 1) cycle elimination, 2) unfolding of contractions, 3) elimination of cuts in the linear fragment.
Cite as

Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing Cycles from Proofs. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{alertubella_et_al:LIPIcs.CSL.2017.9,
  author =	{Aler Tubella, Andrea and Guglielmi, Alessio and Ralph, Benjamin},
  title =	{{Removing Cycles from Proofs}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.9},
  URN =		{urn:nbn:de:0030-drops-77008},
  doi =		{10.4230/LIPIcs.CSL.2017.9},
  annote =	{Keywords: proof theory, deep inference, proof complexity}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.135
A Proof Calculus Which Reduces Syntactic Bureaucracy

Authors: Alessio Guglielmi, Tom Gundersen, and Michel Parigot

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
In usual proof systems, like the sequent calculus, only a very limited way of combining proofs is available through the tree structure. We present in this paper a logic-independent proof calculus, where proofs can be freely composed by connectives, and prove its basic properties. The main advantage of this proof calculus is that it allows to avoid certain types of syntactic bureaucracy inherent to all usual proof systems, in particular the sequent calculus. Proofs in this system closely reflect their atomic flow, which traces the behaviour of atoms through structural rules. The general definition is illustrated by the standard deep-inference system for propositional logic, for which there are known rewriting techniques that achieve cut elimination based only on the information in atomic flows.
Cite as

Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A Proof Calculus Which Reduces Syntactic Bureaucracy. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 135-150, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{guglielmi_et_al:LIPIcs.RTA.2010.135,
  author =	{Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel},
  title =	{{A Proof Calculus Which Reduces Syntactic Bureaucracy}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{135--150},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.135},
  URN =		{urn:nbn:de:0030-drops-26490},
  doi =		{10.4230/LIPIcs.RTA.2010.135},
  annote =	{Keywords: Logic, Proof theory, Deep Inference, Flow graphs, Proof Systems, Open Deduction, Rewriting, Confluence, Termination}
}
  • Refine by Type
  • 6 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2022
  • 1 2017
  • 1 2010

  • Refine by Author
  • 3 Guglielmi, Alessio
  • 2 Ralph, Benjamin
  • 1 Aler Tubella, Andrea
  • 1 Barrett, Victoria
  • 1 Gundersen, Tom
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Linear logic
  • 2 Theory of computation → Proof theory
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Program analysis
  • 1 Theory of computation → Quantum computation theory
  • Show More...

  • Refine by Keyword
  • 2 Proof theory
  • 2 linear logic
  • 1 Binary sessions
  • 1 Causality
  • 1 Confluence
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact