Search

• < Previous
• 1
• Next >

---

A Recipe for State-and-Effect Triangles

Bart Jacobs.

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 capture this situation categorically, involving an adjunction between state- and predicate-transformers. The&nbsp;[&hellip;]

---

Hyper Normalisation and Conditioning for Discrete Probability Distributions

Bart Jacobs.

Normalisation in probability theory turns a subdistribution into a proper distribution. It is a partial operation, since it is undefined for the zero subdistribution. This partiality makes it hard to reason equationally about normalisation. A novel description of normalisation is given as a&nbsp;[&hellip;]

---

From Kleisli Categories to Commutative C*-algebras: Probabilistic Gelfand Duality

Robert W. J. Furber ; Bart P. F. Jacobs.

C*-algebras form rather general and rich mathematical structures that can be studied with different morphisms (preserving multiplication, or not), and with different properties (commutative, or not). These various options can be used to incorporate various styles of computation (set-theoretic,&nbsp;[&hellip;]

---

New Directions in Categorical Logic, for Classical, Probabilistic and Quantum Logic

Bart Jacobs.

Intuitionistic logic, in which the double negation law not-not-P = P fails, is dominant in categorical logic, notably in topos theory. This paper follows a different direction in which double negation does hold. The algebraic notions of effect algebra/module that emerged in theoretical physics form&nbsp;[&hellip;]

---

Featherweight VeriFast

Bart Jacobs ; Frédéric Vogels ; Frank Piessens.

VeriFast is a leading research prototype tool for the sound modular verification of safety and correctness properties of single-threaded and multithreaded C and Java programs. It has been used as a vehicle for exploration and validation of novel program verification techniques and for industrial&nbsp;[&hellip;]

---

Generic Trace Semantics via Coinduction

Ichiro Hasuo ; Bart Jacobs ; Ana Sokolova.

Trace semantics has been defined for various kinds of state-based systems, notably with different forms of branching such as non-determinism vs. probability. In this paper we claim to identify one underlying mathematical structure behind these "trace semantics," namely coinduction in a Kleisli&nbsp;[&hellip;]

---

Orthomodular lattices, Foulis Semigroups and Dagger Kernel Categories

Bart Jacobs.

This paper is a sequel to arXiv:0902.2355 and continues the study of quantum logic via dagger kernel categories. It develops the relation between these categories and both orthomodular lattices and Foulis semigroups. The relation between the latter two notions has been uncovered in the 1960s. The&nbsp;[&hellip;]

---