Search Results

Documents authored by Jacobs, Bart

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/LIPIcs.ECOOP.2019.19
Transferring Obligations Through Synchronizations

Authors: Jafar Hamin and Bart Jacobs

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only performs the actions for which it has permissions and it also fulfills all of its obligations before it terminates. Although permissions can be transferred through synchronizations from a sender thread, where for example a message is sent or a condition variable is notified, to a receiver thread, where that message or that notification is received, in existing approaches obligations can only be transferred when a thread is forked. In this paper we introduce two mechanisms, one for channels and the other for condition variables, that allow obligations, along with permissions, to be transferred from the sender to the receiver, while ensuring that there is no state where the transferred obligations are lost, i.e. where they are discharged from the sender thread but not loaded onto the receiver thread yet. We show how these mechanisms can be used to modularly verify deadlock-freedom of a number of interesting programs, such as some variations of client-server programs, fair readers-writers locks, and dining philosophers, which cannot be modularly verified without such transfer. We also encoded the proposed separation logic-based proof rules in the VeriFast program verifier and succeeded in verifying the mentioned programs.
Cite as

Jafar Hamin and Bart Jacobs. Transferring Obligations Through Synchronizations. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 19:1-19:58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{hamin_et_al:LIPIcs.ECOOP.2019.19,
  author =	{Hamin, Jafar and Jacobs, Bart},
  title =	{{Transferring Obligations Through Synchronizations}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{19:1--19:58},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.19},
  URN =		{urn:nbn:de:0030-drops-108113},
  doi =		{10.4230/LIPIcs.ECOOP.2019.19},
  annote =	{Keywords: Hoare logic, separation logic, modular program verification, synchronization, transferring obligations, deadlock-freedom}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2015.1
A Type Theory for Probabilistic and Bayesian Reasoning

Authors: Robin Adams and Bart Jacobs

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Abstract
This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.
Cite as

Robin Adams and Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 1:1-1:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{adams_et_al:LIPIcs.TYPES.2015.1,
  author =	{Adams, Robin and Jacobs, Bart},
  title =	{{A Type Theory for Probabilistic and Bayesian Reasoning}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{1:1--1:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.1},
  URN =		{urn:nbn:de:0030-drops-84714},
  doi =		{10.4230/LIPIcs.TYPES.2015.1},
  annote =	{Keywords: Probabilistic programming, probabilistic algorithm, type theory, effect module, Bayesian reasoning}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.21
A Formal Semantics of Influence in Bayesian Reasoning

Authors: Bart Jacobs and Fabio Zanasi

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
This paper proposes a formal definition of influence in Bayesian reasoning, based on the notions of state (as probability distribution), predicate, validity and conditioning. Our approach highlights how conditioning a joint entwined/entangled state with a predicate on one of its components has 'crossover' influence on the other components. We use the total variation metric on probability distributions to quantitatively measure such influence. These insights are applied to give a rigorous explanation of the fundamental concept of d-separation in Bayesian networks.
Cite as

Bart Jacobs and Fabio Zanasi. A Formal Semantics of Influence in Bayesian Reasoning. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 21:1-21:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{jacobs_et_al:LIPIcs.MFCS.2017.21,
  author =	{Jacobs, Bart and Zanasi, Fabio},
  title =	{{A Formal Semantics of Influence in Bayesian Reasoning}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{21:1--21:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.21},
  URN =		{urn:nbn:de:0030-drops-80896},
  doi =		{10.4230/LIPIcs.MFCS.2017.21},
  annote =	{Keywords: probability distribution, Bayesian network, influence}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.25
The EfProb Library for Probabilistic Calculations

Authors: Kenta Cho and Bart Jacobs

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
EfProb is an abbreviation of Effectus Probability. It is the name of a library for probability calculations in Python. EfProb offers a uniform language for discrete, continuous and quantum probability. For each of these three cases, the basic ingredients of the language are states, predicates, and channels. Probabilities are typically calculated as validities of predicates in states. States can be updated (conditioned) with predicates. Channels can be used for state transformation and for predicate transformation. This short paper gives an overview of the use of EfProb.
Cite as

Kenta Cho and Bart Jacobs. The EfProb Library for Probabilistic Calculations. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 25:1-25:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cho_et_al:LIPIcs.CALCO.2017.25,
  author =	{Cho, Kenta and Jacobs, Bart},
  title =	{{The EfProb Library for Probabilistic Calculations}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{25:1--25:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo 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.CALCO.2017.25},
  URN =		{urn:nbn:de:0030-drops-80529},
  doi =		{10.4230/LIPIcs.CALCO.2017.25},
  annote =	{Keywords: probability, embedded language, effectus theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.30
Category Theory in Coq 8.5

Authors: Amin Timany and Bart Jacobs

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
We report on our experience implementing category theory in Coq 8.5. Our work formalizes most of basic category theory, including concepts not covered by existing formalizations, in a library that is fit to be used as a general-purpose category-theoretical foundation. Our development particularly takes advantage of two features new to Coq 8.5: primitive projections for records and universe polymorphism. Primitive projections allow for well-behaved dualities while universe polymorphism provides a relative notion of largeness and smallness. The latter is one of the main contributions of this paper. It pushes the limits of the new universe polymorphism and constraint inference algorithm of Coq 8.5. In this paper we present in detail smallness and largeness in categories and the foundation they are built on top of. We furthermore explain how we have used the universe polymorphism of Coq 8.5 to represent smallness and largeness arguments by simply ignoring them and entrusting them to the universe inference algorithm of Coq 8.5. We also briefly discuss our experience throughout this implementation, discuss concepts formalized in this development and give a comparison with a few other developments of similar extent.
Cite as

Amin Timany and Bart Jacobs. Category Theory in Coq 8.5. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{timany_et_al:LIPIcs.FSCD.2016.30,
  author =	{Timany, Amin and Jacobs, Bart},
  title =	{{Category Theory in Coq 8.5}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.30},
  URN =		{urn:nbn:de:0030-drops-60003},
  doi =		{10.4230/LIPIcs.FSCD.2016.30},
  annote =	{Keywords: Category Theory, Coq 8.5, Universe Polymorphism, Homotopy Type Theory}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.116
A Recipe for State-and-Effect Triangles

Authors: Bart Jacobs

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

Abstract
In the semantics of programming languages one can view programs as state transformers, or as predicate transformers. Recently the author has introduced 'state-and-effect' triangles which captures this situation categorically, involving an adjunction between state- and predicate-transformers. The current paper exploits a classical result in category theory, part of Jon Beck's monadicity theorem, to systematically construct such a state-and-effect triangle from an adjunction. The power of this construction is illustrated in many examples, both for the Boolean and probabilistic (quantitative) case.
Cite as

Bart Jacobs. A Recipe for State-and-Effect Triangles. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 116-129, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{jacobs:LIPIcs.CALCO.2015.116,
  author =	{Jacobs, Bart},
  title =	{{A Recipe for State-and-Effect Triangles}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{116--129},
  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.116},
  URN =		{urn:nbn:de:0030-drops-55301},
  doi =		{10.4230/LIPIcs.CALCO.2015.116},
  annote =	{Keywords: Duality, predicate transformer, state transformer, state-and-effect triangle}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.664
Modular Termination Verification

Authors: Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. We start from an existing program logic for partial correctness based on separation logic and abstract predicate families. We extend it with call permissions qualified by an arbitrary ordinal number, and we define a specification style that properly hides implementation details, based on the ideas of using methods and bags of methods as ordinals, and exposing the bag of methods reachable from an object as an abstract predicate argument. These enable each method to abstractly request permission to call all methods reachable by it any finite number of times, and to delegate similar permissions to its callees. We illustrate the approach with several examples.
Cite as

Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. Modular Termination Verification. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 664-688, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{jacobs_et_al:LIPIcs.ECOOP.2015.664,
  author =	{Jacobs, Bart and Bosnacki, Dragan and Kuiper, Ruurd},
  title =	{{Modular Termination Verification}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{664--688},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.664},
  URN =		{urn:nbn:de:0030-drops-52422},
  doi =		{10.4230/LIPIcs.ECOOP.2015.664},
  annote =	{Keywords: Termination, program verification, modular verification, separation logic, well-founded relations}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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