text: abstract
  we develop the operational semantics of an untyped probabilistic λ-calculus with continuous distributions, and both hard and soft constraints, as a foundation for universal probabilistic programming languages such as church, anglican, and venture. our first contribution
  is to adapt the classic operational semantics of λ-calculus to a continuous setting via creating
  a measure space on terms and defining step-indexed approximations. we prove equivalence of
  big-step and small-step formulations of this distribution-based semantics. to move closer to
  inference techniques, we also define the sampling-based semantics of a term as a function from
  a trace of random samples to a value. we show that the distribution induced by integration
  over the space of traces equals the distribution-based semantics. our second contribution is
  to formalize the implementation technique of trace markov chain monte carlo (mcmc) for
  our calculus and to show its correctness. a key step is defining sufficient conditions for the
  distribution induced by trace mcmc to converge to the distribution-based semantics. to
  the best of our knowledge, this is the first rigorous correctness proof for trace mcmc for a
  higher-order functional language, or for a language with soft constraints.