  We study termination of higher-order probabilistic functional programs with
recursion, stochastic conditioning and sampling from continuous distributions.
  Reasoning about the termination probability of programs with continuous
distributions is hard, because the enumeration of terminating executions cannot
provide any non-trivial bounds. We present a new operational semantics based on
traces of intervals, which is sound and complete with respect to the standard
sampling-based semantics, in which (countable) enumeration can provide
arbitrarily tight lower bounds. Consequently we obtain the first proof that
deciding almost-sure termination (AST) for programs with continuous
distributions is $\Pi^0_2$-complete. We also provide a compositional
representation of our semantics in terms of an intersection type system.
  In the second part, we present a method of proving AST for non-affine
programs, i.e., recursive programs that can, during the evaluation of the
recursive body, make multiple recursive calls (of a first-order function) from
distinct call sites. Unlike in a deterministic language, the number of
recursion call sites has direct consequences on the termination probability.
Our framework supports a proof system that can verify AST for programs that are
well beyond the scope of existing methods.
  We have constructed prototype implementations of our method of computing
lower bounds of termination probability, and AST verification.
