  We extend the simply-typed guarded $\lambda$-calculus with discrete
probabilities and endow it with a program logic for reasoning about relational
properties of guarded probabilistic computations. This provides a framework for
programming and reasoning about infinite stochastic processes like Markov
chains. We demonstrate the logic sound by interpreting its judgements in the
topos of trees and by using probabilistic couplings for the semantics of
relational assertions over distributions on discrete types.
  The program logic is designed to support syntax-directed proofs in the style
of relational refinement types, but retains the expressiveness of higher-order
logic extended with discrete distributions, and the ability to reason
relationally about expressions that have different types or syntactic
structure. In addition, our proof system leverages a well-known theorem from
the coupling literature to justify better proof rules for relational reasoning
about probabilistic expressions. We illustrate these benefits with a broad
range of examples that were beyond the scope of previous systems, including
shift couplings and lump couplings between random walks.
