Document Open Access Logo

Proof Identity and Categorical Models of BV

Authors Matteo Acclavio , Lutz Straßburger , Vladimir Zamdzhiev

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.3.pdf
  • Filesize: 0.9 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • BV
  • Categorical Semantics
  • Denotational Semantics

Metrics

Abstract

BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-defined notion of proof identity for BV on the other side, the precise relation between BV-categories and the logic BV is still not clear. To improve on this situation, we define in this paper a notion of proof identity for BV, based on the notion of atomic flows, which can be seen as a special form of string diagrams. Based on this notion of proof identity, we then strengthen the existing notion of BV-category and prove that it is sound with respect to the logic.

Cite As Get BibTex

Matteo Acclavio, Lutz Straßburger, and Vladimir Zamdzhiev. Proof Identity and Categorical Models of BV. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.3

Author Details

Matteo Acclavio
  • FORM, University of Southern Denmark, Odense, Denmark
  • University of Sussex, UK
Lutz Straßburger
  • Inria, LIX, Ecole Polytechnique, Institut Polytechnique Paris, France
Vladimir Zamdzhiev
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

Funding

  • Straßburger, Lutz: Partially supported by the French Ministry for Europe and Foreign Affairs (MEAE), the Embassy of France in the UK, and the French Ministry of Higher Education and Research (MESR), via the PHC Sophie Germain project "Using Formal Logic to Reduce Bias in Large Language Models"
  • Zamdzhiev, Vladimir: This work has been partially funded by the French National Research Agency (ANR) within the framework of "Plan France 2030", under the research projects EPIQ ANR-22-PETQ-0007, HQI-Acquisition ANR-22-PNCQ-0001, and HQI-R&D ANR-22-PNCQ-0002.

Acknowledgements

We thank the anonymous referees for their feedback which led to multiple improvements to the paper. We also thank James Hefford for discussions related to this paper.

References

  1. Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59(2):543-574, 1994. URL: https://doi.org/10.2307/2275407.
  2. Matteo Acclavio and Lutz Strassburger. Intuitionistic BV (extended version), 2025. URL: https://doi.org/10.48550/arXiv.2505.13284.
  3. Matteo Acclavio and Lutz Straßburger. Intuitionistic BV. In Gian Luca Pozzato and Tarmo Uustalu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 414-432, Cham, 2026. Springer Nature Switzerland. Google Scholar
  4. Matteo Acclavio, Lutz Straßburger, and Vladimir Zamdzhiev. Proof identity and categorical models of BV, 2026. URL: https://arxiv.org/abs/2604.25501.
  5. Andrea Aler Tubella. A study of normalisation through subatomic logic. PhD thesis, University of Bath, 2016. Google Scholar
  6. Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, and Samuel Mimram. Polygraphs: From Rewriting to Higher Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 2025. Google Scholar
  7. David P. Blecher and Christian Le Merdy. Operator Algebras and Their Modules: An operator space approach. Oxford University Press, October 2004. URL: https://doi.org/10.1093/acprof:oso/9780198526599.001.0001.
  8. Richard Blute. Linear logic, coherence and dinaturality. Theoretical Computer Science, 115:3-41, 1993. URL: https://doi.org/10.1016/0304-3975(93)90053-V.
  9. Richard Blute, Prakash Panangaden, and Sergey Slavnov. Deep inference and probabilistic coherence spaces. Applied Categorical Structures, 20(3):209-228, 2012. URL: https://doi.org/10.1007/s10485-010-9241-0.
  10. Richard F. Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden, and Lutz Straßburger. A logical basis for quantum evolution and entanglement. In Claudia Casadio, Bob Coecke, Michael Moortgat, and Philip Scott, editors, Categories and Types in Logic, Language, and Physics: Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, pages 90-107. Springer Berlin Heidelberg, Berlin, Heidelberg, 2014. URL: https://doi.org/10.1007/978-3-642-54789-8_6.
  11. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: Rewriting with Frobenius structure. J. ACM, 69(2), March 2022. URL: https://doi.org/10.1145/3502719.
  12. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory II: Rewriting with symmetric monoidal structure. Mathematical Structures in Computer Science, 32(4):511-541, 2022. URL: https://doi.org/10.1017/S0960129522000317.
  13. Paola Bruscoli. A purely logical account of sequentiality in proof search. In International Conference on Logic Programming, pages 302-316. Springer, 2002. URL: https://doi.org/10.1007/3-540-45619-8_21.
  14. Alessandra Carbone. Turning cycles into spirals. Ann. Pure Appl. Logic, 96(1-3):57-73, 1999. URL: https://doi.org/10.1016/S0168-0072(98)00031-1.
  15. J.R.B. Cockett, M. Hasegawa, and R.A.G. Seely. Coherence of the double involution on *-autonomous categories. Theory and Applications of Categories, 17(2):17-29, 2006. Google Scholar
  16. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 209(6):966-991, 2011. URL: https://doi.org/10.1016/j.ic.2011.02.001.
  17. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28(3):181-203, 1989. URL: https://doi.org/10.1007/BF01622878.
  18. Edward G. Effros and Zhong-Jin Ruan. Operator space tensor products and Hopf convolution algebras. Journal of Operator Theory, 50(1):131-156, 2003. URL: http://www.jstor.org/stable/24718935.
  19. E.G. Effros and Z.J. Ruan. Operator Spaces. London Mathematical Society monographs. Clarendon Press, 2000. URL: https://books.google.fr/books?id=v7mj8Dy84k8C.
  20. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full abstraction for probabilistic PCF. J. ACM, 65(4):23:1-23:44, 2018. URL: https://doi.org/10.1145/3164540.
  21. Thomas Ehrhard and Christine Tasson. Probabilistic call by push value. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:3)2019.
  22. Arnaud Fleury and Christian Retoré. The mix rule. Mathematical Structures in Computer Science, 4(2):273-285, 1994. URL: https://doi.org/10.1017/S0960129500000451.
  23. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  24. Jean-Yves Girard. Proof-nets : the parallel syntax for proof-theory. In Aldo Ursini and Paolo Agliano, editors, Logic and Algebra. Marcel Dekker, New York, 1996. Google Scholar
  25. Jean-Yves Girard. Between logic and quantic: a tract. Linear Logic in Computer Science, London Mathematical Society Lecture Notes Series, 316, 2004. Google Scholar
  26. Alessio Guglielmi. A system of interaction and structure. ACM Trans. Comput. Logic, 8(1), January 2007. URL: https://doi.org/10.1145/1182613.1182614.
  27. Alessio Guglielmi and Tom Gundersen. Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science, 4(1:9), March 2008. URL: https://doi.org/10.2168/LMCS-4(1:9)2008.
  28. Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A Proof Calculus Which Reduces Syntactic Bureaucracy. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 135-150, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.RTA.2010.135.
  29. Alessio Guglielmi, Tom Gundersen, and Lutz Straßburger. Breaking paths in atomic flows for classical logic. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 284-293. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.12.
  30. Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the calculus of structures. In Laurent Fribourg, editor, Computer Science Logic, CSL 2001, volume 2142 of LNCS, pages 54-68. Springer-Verlag, 2001. URL: https://doi.org/10.1007/3-540-44802-0_5.
  31. Alessio Guglielmi and Lutz Straßburger. A system of interaction and structure V: the exponentials and splitting. Math. Struct. Comput. Sci., 21(3):563-584, 2011. URL: https://doi.org/10.1017/S096012951100003X.
  32. James Hefford and Matthew Wilson. A BV-category of spacetime interventions. CoRR, abs/2502.19022, 2025. URL: https://doi.org/10.48550/arXiv.2502.19022.
  33. Chris Heunen and Jamie Vicary. Categories for Quantum Theory: An Introduction. Oxford University Press, November 2019. URL: https://doi.org/10.1093/oso/9780198739623.001.0001.
  34. Ross Horne and Alwen Tiu. Constructing weak simulations from linear implications for processes with private names. Mathematical Structures in Computer Science, 29(8):1275-1308, 2019. URL: https://doi.org/10.1017/S0960129518000452.
  35. Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. Private Names in Non-Commutative Logic. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory (CONCUR 2016), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.31.
  36. Dominic Hughes. Simple free star-autonomous categories and full coherence, 2005. Preprint. URL: https://arxiv.org/abs/math/0506521.
  37. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science, 294(1):183-231, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00241-9.
  38. Gregory Maxwell Kelly and M. L. Laplaza. Coherence for compact closed categories. J. of Pure and Applied Algebra, 19:193-213, 1980. Google Scholar
  39. Gregory Maxwell Kelly and Saunders Mac Lane. Coherence in closed categories. J. of Pure and Applied Algebra, 1:97-140, 1971. Google Scholar
  40. Yves Lafont. Towards an algebraic theory of boolean circuits. Journal of Pure and Applied Algebra, 184(2):257-310, 2003. URL: https://doi.org/10.1016/S0022-4049(03)00069-0.
  41. François Lamarche and Lutz Straßburger. From proof nets to the free *-autonomous category. Logical Methods in Computer Science, 2(4:3):1-44, 2006. URL: https://doi.org/10.2168/LMCS-2(4:3)2006.
  42. Saunders Mac Lane. Categories for the working mathematician. Springer New York, NY, 1978. URL: https://doi.org/10.1007/978-1-4757-4721-8.
  43. Thea Li and Vladimir Zamdzhiev. Quantum coherence spaces revisited: A von Neumann (co)algebraic approach. In Nathalie Bertrand and Stefan Milius, editors, Foundations of Software Science and Computation Structures - 29th International Conference, FoSSaCS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Lecture Notes in Computer Science, pages 418-439. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22730-0_20.
  44. Bert Lindenhovius and Vladimir Zamdzhiev. The category of operator spaces and complete contractions. CoRR, abs/2412.20999, 2024. URL: https://doi.org/10.48550/arXiv.2412.20999.
  45. Bert Lindenhovius and Vladimir Zamdzhiev. Operator spaces, linear logic and the Heisenberg-Schrödinger duality of quantum theory. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 870-883. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00071.
  46. Lê Thành Dung Nguyên and Lutz Straßburger. A system of interaction and structure III: the complexity of BV and pomset logic. Log. Methods Comput. Sci., 19(4), 2023. URL: https://doi.org/10.46298/LMCS-19(4:25)2023.
  47. Lê Thành Dũng Nguyên and Lutz Straßburger. BV and Pomset Logic are not the same. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1-3:17, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.3.
  48. Gilles Pisier. Introduction to Operator Space Theory. London Mathematical Society Lecture Note Series. Cambridge University Press, 2003. Google Scholar
  49. Samuel R. Buss. The undecidability of k-provability. Annals of Pure and Applied Logic, 53(1):75-102, 1991. URL: https://doi.org/10.1016/0168-0072(91)90059-U.
  50. Christian Retoré. Réseaux et Séquents Ordonnés. PhD thesis, Université Paris VII, 1993. Google Scholar
  51. Christian Retoré. A semantic characterisation of the correctness of a proof net. Mathematical Structures in Computer Science, 7(5):445-452, 1997. URL: https://doi.org/10.1017/S096012959700234X.
  52. Christian Retoré. Pomset logic as a calculus of directed cographs. In V. M. Abrusci and C. Casadio, editors, Dynamic Perspectives in Logic and Linguistics, pages 221-247. Bulzoni, Roma, 1999. Also available as INRIA Rapport de Recherche RR-3714. Google Scholar
  53. Christian Retoré. Pomset logic: The other approach to noncommutativity in logic. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, pages 299-345, 2021. Google Scholar
  54. Peter Selinger. Dagger compact closed categories and completely positive maps: (extended abstract). Electronic Notes in Theoretical Computer Science, 170:139-163, 2007. Proceedings of the 3rd International Workshop on Quantum Programming Languages (QPL 2005). URL: https://doi.org/10.1016/j.entcs.2006.12.018.
  55. Will Simmons. Causal types for higher-order quantum theory. PhD thesis, University of Oxford, 2024. Google Scholar
  56. Will Simmons and Aleks Kissinger. Higher-order causal theories are models of BV-logic. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), volume 241 of Leibniz International Proceedings in Informatics (LIPIcs), pages 80:1-80:14, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.80.
  57. Will Simmons and Aleks Kissinger. A complete logic for causal consistency, 2024. URL: https://doi.org/10.48550/arXiv.2403.09297.
  58. Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: The exponentials and decomposition. ACM Trans. Comput. Logic, 12(4), July 2011. URL: https://doi.org/10.1145/1970398.1970399.
  59. Alwen Fernanto Tiu. A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science, 2(2):1-24, 2006. URL: https://doi.org/10.2168/LMCS-2(2:4)2006.
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