A Type Theory for Probabilistic { extdollar}{ extdollar}{ extbackslash}lambda { extdollar}{ extdollar}{ extendash}calculus

We present a theory of types where formulas may contain a choice constructor. This constructor allows for the selection of a particular type among a finite set of options, each corresponding to a given probabilistic term. We show that this theory induces a type assignment system for the probabilistic λ –calculus introduced in an earlier work by Chris Hankin, Herbert Wiklicky and the author, where probabilistic terms represent probability distributions on classical terms of the simply typed λ –calculus. We prove the soundness of the type assignment with respect to a probabilistic term reduction and a normalization property of the latter.