Coupling proofs are probabilistic product programs | Publicación