DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.3

Proof Identity and Categorical Models of BV

Authors: Matteo Acclavio, Lutz Straßburger, and Vladimir Zamdzhiev

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{acclavio_et_al:LIPIcs.FSCD.2026.3,
  author =	{Acclavio, Matteo and Stra{\ss}burger, Lutz and Zamdzhiev, Vladimir},
  title =	{{Proof Identity and Categorical Models of BV}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{3:1--3:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.3},
  URN =		{urn:nbn:de:0030-drops-263532},
  doi =		{10.4230/LIPIcs.FSCD.2026.3},
  annote =	{Keywords: BV, Categorical Semantics, Denotational Semantics}
}

Document

Early Ideas

DOI: 10.4230/LIPIcs.CALCO.2021.18

The Central Valuations Monad (Early Ideas)

Authors: Xiaodong Jia, Michael Mislove, and Vladimir Zamdzhiev

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract

We give a commutative valuations monad Z on the category DCPO of dcpo’s and Scott-continuous functions. Compared to the commutative valuations monads given in [Xiaodong Jia et al., 2021], our new monad Z is larger and it contains all push-forward images of valuations on the unit interval [0, 1] along lower semi-continuous maps. We believe that this new monad will be useful in giving domain-theoretic denotational semantics for statistical programming languages with continuous probabilistic choice.

Cite as

Xiaodong Jia, Michael Mislove, and Vladimir Zamdzhiev. The Central Valuations Monad (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 18:1-18:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{jia_et_al:LIPIcs.CALCO.2021.18,
  author =	{Jia, Xiaodong and Mislove, Michael and Zamdzhiev, Vladimir},
  title =	{{The Central Valuations Monad}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{18:1--18:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio 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.CALCO.2021.18},
  URN =		{urn:nbn:de:0030-drops-153733},
  doi =		{10.4230/LIPIcs.CALCO.2021.18},
  annote =	{Keywords: Valuations, Commutative Monad, DCPO, Probabilistic Choice, Recursion}
}

Search Results

Documents authored by Zamdzhiev, Vladimir

Proof Identity and Categorical Models of BV

Abstract

Cite as

The Central Valuations Monad (Early Ideas)

Abstract

Cite as

Thanks for your feedback!

Could not send message