3 Search Results for "Voorneveld, Niels F. W."

Document
DOI: 10.4230/LIPIcs.CSL.2026.28
Resourceful Traces for Commuting Processes

Authors: Matthew Earnshaw, Chad Nester, and Mario Román

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We show that, when the actions of a Mazurkiewicz trace are considered not merely as atomic but as transformations from a specified type of inputs to a specified type of outputs, we obtain a novel notion of presentation for effectful categories (also known as generalized Freyd categories), a well-known algebraic structure in the semantics of side-effecting computation. Like the usual representation of traces as graphs, our notion of presentation gives rise to a graphical representation of morphisms in effectful categories. We use our presentations to give a construction of the commuting tensor product of free effectful categories, capturing the combination of systems in which the actions of each must commute with one another, while still permitting exchange of resources.
Cite as

Matthew Earnshaw, Chad Nester, and Mario Román. Resourceful Traces for Commuting Processes. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{earnshaw_et_al:LIPIcs.CSL.2026.28,
  author =	{Earnshaw, Matthew and Nester, Chad and Rom\'{a}n, Mario},
  title =	{{Resourceful Traces for Commuting Processes}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.28},
  URN =		{urn:nbn:de:0030-drops-254522},
  doi =		{10.4230/LIPIcs.CSL.2026.28},
  annote =	{Keywords: Mazurkiewicz traces, premonoidal categories, monoidal categories, effectful categories}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.29
Parametric Iteration in Resource Theories

Authors: Alessandro Di Giorgio, Pawel Sobocinski, and Niels Voorneveld

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Many algorithms are specified with respect to a fixed but unknown parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key. Our aim is to capture this phenomenon in a more abstract setting. We focus on resource theories - general calculi of processes with a string diagrammatic syntax - introducing a general parametric iteration construction. By instantiating this construction within the Markov category of probabilistic Boolean circuits and equipping it with a suitable metric, we are able to capture the notion of negligibility via asymptotic equivalence, in a compositional way. This allows us to use diagrammatic reasoning to prove simple cryptographic theorems - for instance, proving that guessing a randomly generated key has negligible success.
Cite as

Alessandro Di Giorgio, Pawel Sobocinski, and Niels Voorneveld. Parametric Iteration in Resource Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{digiorgio_et_al:LIPIcs.CSL.2026.29,
  author =	{Di Giorgio, Alessandro and Sobocinski, Pawel and Voorneveld, Niels},
  title =	{{Parametric Iteration in Resource Theories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{29:1--29:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.29},
  URN =		{urn:nbn:de:0030-drops-254541},
  doi =		{10.4230/LIPIcs.CSL.2026.29},
  annote =	{Keywords: Markov categories, Cryptography, String diagrams, Asymptotic equivalence}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.31
Slice Nondeterminism

Authors: Niels F. W. Voorneveld

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
This paper studies a technique for describing and formalising nondeterministic functions, using slice categories. Results of a nondeterministic function are modelled by an object of the slice category over the codomain of the function, which is an indexed family over the codomain. Two such families denote the same set of results if slice morphisms exist between them in both directions. We formulate the category of nondeterministic functions by expressing a set of possible results as an equivalence class of objects. If we allow families to use any indexing set, this category will be equivalent to the category of relations. When we limit ourselves to a smaller universe of indexing sets, we get a subcategory which more closely resembles nondeterministic programs. We compare this category with other representations of the category of relations, and see how many properties can be carried over, such as its product, coproduct and other monoidal structures. We can describe inductive nondeterministic structures by lifting free monads from the category of sets. Moreover, due to the intensional nature of the slice representation, nondeterministic processes are easily represented, such as interleaving concurrency and labelled transition systems. This paper has been formalised in Agda.
Cite as

Niels F. W. Voorneveld. Slice Nondeterminism. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{voorneveld:LIPIcs.ITP.2023.31,
  author =	{Voorneveld, Niels F. W.},
  title =	{{Slice Nondeterminism}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.31},
  URN =		{urn:nbn:de:0030-drops-184063},
  doi =		{10.4230/LIPIcs.ITP.2023.31},
  annote =	{Keywords: Category theory, Agda, Slice category, Nondeterministic functions, Powerset}
}
  • Refine by Type
  • 3 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 1 2023

  • Refine by Author
  • 1 Di Giorgio, Alessandro
  • 1 Earnshaw, Matthew
  • 1 Nester, Chad
  • 1 Román, Mario
  • 1 Sobocinski, Pawel
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Categorical semantics
  • 1 Mathematics of computing → Probability and statistics
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Program semantics
  • Show More...

  • Refine by Keyword
  • 1 Agda
  • 1 Asymptotic equivalence
  • 1 Category theory
  • 1 Cryptography
  • 1 Markov categories
  • 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