7 Search Results for "Pavlovic, Dusko"

Document
DOI: 10.4230/LIPIcs.CSL.2025.28
Strong Induction Is an Up-To Technique

Authors: Filippo Bonchi, Elena Di Lavore, and Anna Ricci

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

Abstract
Up-to techniques are enhancements of the coinduction proof principle which, in lattice theoretic terms, is the dual of induction. What is the dual of coinduction up-to? By means of duality, we illustrate a theory of induction up-to and we observe that an elementary proof technique, commonly known as strong induction, is an instance of induction up-to. We also show that, when generalising our theory from lattices to categories, one obtains an enhancement of the induction definition principle known in the literature as comonadic recursion.
Cite as

Filippo Bonchi, Elena Di Lavore, and Anna Ricci. Strong Induction Is an Up-To Technique. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CSL.2025.28,
  author =	{Bonchi, Filippo and Di Lavore, Elena and Ricci, Anna},
  title =	{{Strong Induction Is an Up-To Technique}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{28:1--28:21},
  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.28},
  URN =		{urn:nbn:de:0030-drops-227856},
  doi =		{10.4230/LIPIcs.CSL.2025.28},
  annote =	{Keywords: Induction, Coinduction, Up-to Techniques, Induction up-to, Lattices, Algebras}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2023.13
A Category for Unifying Gaussian Probability and Nondeterminism

Authors: Dario Stein and Richard Samuelson

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract
We introduce categories of extended Gaussian maps and Gaussian relations which unify Gaussian probability distributions with relational nondeterminism in the form of linear relations. Both have crucial and well-understood applications in statistics, engineering, and control theory, but combining them in a single formalism is challenging. It enables us to rigorously describe a variety of phenomena like noisy physical laws, Willems' theory of open systems and uninformative priors in Bayesian statistics. The core idea is to formally admit vector subspaces D ⊆ X as generalized uniform probability distribution. Our formalism represents a first bridge between the literature on categorical systems theory (signal-flow diagrams, linear relations, hypergraph categories) and notions of probability theory.
Cite as

Dario Stein and Richard Samuelson. A Category for Unifying Gaussian Probability and Nondeterminism. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{stein_et_al:LIPIcs.CALCO.2023.13,
  author =	{Stein, Dario and Samuelson, Richard},
  title =	{{A Category for Unifying Gaussian Probability and Nondeterminism}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.13},
  URN =		{urn:nbn:de:0030-drops-188107},
  doi =		{10.4230/LIPIcs.CALCO.2023.13},
  annote =	{Keywords: systems theory, hypergraph categories, Bayesian inference, category theory, Markov categories}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.28
Counting and Matching

Authors: Bart Jacobs and Dario Stein

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Lists, multisets and partitions are fundamental datatypes in mathematics and computing. There are basic transformations from lists to multisets (called "accumulation") and also from lists to partitions (called "matching"). We show how these transformations arise systematically by forgetting/abstracting away certain aspects of information, namely order (transposition) and identity (substitution). Our main result is that suitable restrictions of these transformations are isomorphisms: This reveals fundamental correspondences between elementary datatypes. These restrictions involve "incremental" lists/multisets and "non-crossing" partitions/lists. While the process of forgetting information can be precisely spelled out in the language of category theory, the relevant constructions are very combinatorial in nature. The lists, partitions and multisets in these constructions are counted by Bell numbers and Catalan numbers. One side-product of our main result is a (terminating) rewriting system that turns an arbitrary partition into a non-crossing partition, without improper nestings.
Cite as

Bart Jacobs and Dario Stein. Counting and Matching. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jacobs_et_al:LIPIcs.CSL.2023.28,
  author =	{Jacobs, Bart and Stein, Dario},
  title =	{{Counting and Matching}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.28},
  URN =		{urn:nbn:de:0030-drops-174892},
  doi =		{10.4230/LIPIcs.CSL.2023.28},
  annote =	{Keywords: List, Multiset, Partition, Crossing}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.4
Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation

Authors: Mila Dalla Preda

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Static and dynamic program analyses attempt to extract useful information on program’s behaviours. Static analysis uses an abstract model of programs to reason on their runtime behaviour without actually running them, while dynamic analysis reasons on a test set of real program executions. For this reason, the precision of static analysis is limited by the presence of false positives (executions allowed by the abstract model that cannot happen at runtime), while the precision of dynamic analysis is limited by the presence of false negatives (real executions that are not in the test set). Researchers have developed many analysis techniques and tools in the attempt to increase the precision of program verification. Software protection is an interesting scenario where programs need to be protected from adversaries that use program analysis to understand their inner working and then exploit this knowledge to perform some illicit actions. Program analysis plays a dual role in program verification and software protection: in program verification we want the analysis to be as precise as possible, while in software protection we want to degrade the results of the analysis as much as possible. Indeed, in software protection researchers usually recur to a special class of program transformations, called code obfuscation, to modify a program in order to make it more difficult to analyse while preserving its intended functionality. In this setting, it is interesting to study how program transformations that preserve the intended behaviour of programs can affect the precision of both static and dynamic analysis. While some works have been done in order to formalise the efficiency of code obfuscation in degrading static analysis and in the possibility of transforming programs in order to avoid or increase false positives, less attention has been posed to formalise the relation between program transformations and false negatives in dynamic analysis. In this work we are setting the scene for a formal investigation of the syntactic and semantic program features that affect the presence of false negatives in dynamic analysis. We believe that this understanding would be useful for improving the precision of the existing dynamic analysis tools and in the design of program transformations that complicate the dynamic analysis. To Maurizio on his 60th birthday!
Cite as

Mila Dalla Preda. Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dallapreda:OASIcs.Gabbrielli.4,
  author =	{Dalla Preda, Mila},
  title =	{{Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{4:1--4:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.4},
  URN =		{urn:nbn:de:0030-drops-132263},
  doi =		{10.4230/OASIcs.Gabbrielli.4},
  annote =	{Keywords: Program analysis, analysis precision, program transformation, software protection, code obfuscation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.24
Refinement for Signal Flow Graphs

Authors: Filippo Bonchi, Joshua Holland, Dusko Pavlovic, and Pawel Sobocinski

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
The symmetric monoidal theory of Interacting Hopf Algebras provides a sound and complete axiomatisation for linear relations over a given field. As is the case for ordinary relations, linear relations have a natural order that coincides with inclusion. In this paper, we give a presentation for this ordering by extending the theory of Interacting Hopf Algebras with a single additional inequation. We show that the extended theory gives rise to an abelian bicategory—a concept due to Carboni and Walters—and highlight similarities with the algebra of relations. Most importantly, the ordering leads to a well-behaved notion of refinement for signal flow graphs.
Cite as

Filippo Bonchi, Joshua Holland, Dusko Pavlovic, and Pawel Sobocinski. Refinement for Signal Flow Graphs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2017.24,
  author =	{Bonchi, Filippo and Holland, Joshua and Pavlovic, Dusko and Sobocinski, Pawel},
  title =	{{Refinement for Signal Flow Graphs}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.24},
  URN =		{urn:nbn:de:0030-drops-77758},
  doi =		{10.4230/LIPIcs.CONCUR.2017.24},
  annote =	{Keywords: Signal flow graphs, refinement, operational semantics, string diagrams, symmetric monoidal inequality theory}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.130
Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra

Authors: Toshiki Kataoka and Dusko Pavlovic

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
While computer programs and logical theories begin by declaring the concepts of interest, be it as data types or as predicates, network computation does not allow such global declarations, and requires concept mining and concept analysis to extract shared semantics for different network nodes. Powerful semantic analysis systems have been the drivers of nearly all paradigm shifts on the web. In categorical terms, most of them can be described as bicompletions of enriched matrices, generalizing the Dedekind-MacNeille-style completions from posets to suitably enriched categories. Yet it has been well known for more than 40 years that ordinary categories themselves in general do not permit such completions. Armed with this new semantical view of Dedekind-MacNeille completions, and of matrix bicompletions, we take another look at this ancient mystery. It turns out that simple categorical versions of the limit superior and limit inferior operations characterize a general notion of Dedekind-MacNeille completion, that seems to be appropriate for ordinary categories, and boils down to the more familiar enriched versions when the limits inferior and superior coincide. This explains away the apparent gap among the completions of ordinary categories, and broadens the path towards categorical concept mining and analysis, opened in previous work.
Cite as

Toshiki Kataoka and Dusko Pavlovic. Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 130-155, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kataoka_et_al:LIPIcs.CALCO.2015.130,
  author =	{Kataoka, Toshiki and Pavlovic, Dusko},
  title =	{{Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{130--155},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.130},
  URN =		{urn:nbn:de:0030-drops-55317},
  doi =		{10.4230/LIPIcs.CALCO.2015.130},
  annote =	{Keywords: concept analysis, semantic indexing, category, completion, algebra}
}
Document
DOI: 10.4230/DagSemProc.09311.2
Geometry of abstraction in quantum computation

Authors: Dusko Pavlovic

Published in: Dagstuhl Seminar Proceedings, Volume 9311, Classical and Quantum Information Assurance Foundations and Practice (2010)

Abstract
Modern cryptography is based on various assumptions about computational hardness and feasibility. But while computability is a very robust notion (cf Church's Thesis), feasibility seems quite sensitive to the available computational resources. A prime example are, of course, quantum channels, which provide feasible solutions of some otherwise hard problems; but ants' pheromones, used as a computational resource, also provide feasible solutions of other hard problems. So at least in principle, modern cryptography is concerned with the power and availability of computational resources. The standard models, used in cryptography and in quantum computation, leave a lot to be desired in this respect. They do, of course, support many interesting solutions of deep problems; but besides the fundamental computational structures, they also capture some low level features of particular implementations. In technical terms of program semantics, our standard models are not *fully abstract*. (Related objections can be traced back to von Neumann's "I don't believe in Hilbert spaces" letters from 1937.) I shall report on some explorations towards extending the modeling tools of program semantics to develop a geometric language for quantum protocols and algorithms. Besides hiding the irrelevant implementation details, its abstract descriptions can also be used to explore simple nonstandard models. If the time permits, I shall describe a method to implement teleportation, as well as the hidden subgroup algorithms, using just abelian groups and relations.
Cite as

Dusko Pavlovic. Geometry of abstraction in quantum computation. In Classical and Quantum Information Assurance Foundations and Practice. Dagstuhl Seminar Proceedings, Volume 9311, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{pavlovic:DagSemProc.09311.2,
  author =	{Pavlovic, Dusko},
  title =	{{Geometry of abstraction in quantum computation}},
  booktitle =	{Classical and Quantum Information Assurance Foundations and Practice},
  pages =	{1--28},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9311},
  editor =	{Samual L. Braunstein and Hoi-Kwong Lo and Kenny Paterson and Peter Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09311.2},
  URN =		{urn:nbn:de:0030-drops-23623},
  doi =		{10.4230/DagSemProc.09311.2},
  annote =	{Keywords: Quantum algorithms, categorical semantics, Frobenius algebra, classical structure}
}
  • Refine by Type
  • 7 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2023
  • 1 2020
  • 1 2017
  • 1 2015
  • Show More...

  • Refine by Author
  • 3 Pavlovic, Dusko
  • 2 Bonchi, Filippo
  • 2 Stein, Dario
  • 1 Dalla Preda, Mila
  • 1 Di Lavore, Elena
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs
  • 1 OASIcs
  • 1 DagSemProc

  • Refine by Classification
  • 1 Mathematics of computing → Combinatorics
  • 1 Mathematics of computing → Probability and statistics
  • 1 Security and privacy → Software reverse engineering
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 1 Algebras
  • 1 Bayesian inference
  • 1 Coinduction
  • 1 Crossing
  • 1 Frobenius algebra
  • 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