  Sensitivity properties describe how changes to the input of a program affect
the output, typically by upper bounding the distance between the outputs of two
runs by a monotone function of the distance between the corresponding inputs.
When programs are probabilistic, the distance between outputs is a distance
between distributions. The Kantorovich lifting provides a general way of
defining a distance between distributions by lifting the distance of the
underlying sample space; by choosing an appropriate distance on the base space,
one can recover other usual probabilistic distances, such as the Total
Variation distance. We develop a relational pre-expectation calculus to upper
bound the Kantorovich distance between two executions of a probabilistic
program. We illustrate our methods by proving algorithmic stability of a
machine learning algorithm, convergence of a reinforcement learning algorithm,
and fast mixing for card shuffling algorithms. We also consider some
extensions: proving lower bounds on the Total Variation distance and
convergence to the uniform distribution. Finally, we describe an asynchronous
extension of our calculus to reason about pairs of program executions with
different control flow.
