  Independence and conditional independence are fundamental concepts for
reasoning about groups of random variables in probabilistic programs.
Verification methods for independence are still nascent, and existing methods
cannot handle conditional independence. We extend the logic of bunched
implications (BI) with a non-commutative conjunction and provide a model based
on Markov kernels; conditional independence can be directly captured as a
logical formula in this model. Noting that Markov kernels are Kleisli arrows
for the distribution monad, we then introduce a second model based on the
powerset monad and show how it can capture join dependency, a non-probabilistic
analogue of conditional independence from database theory. Finally, we develop
a program logic for verifying conditional independence in probabilistic
programs.
