  We show that an intuitionistic version of counting propositional logic
corresponds, in the sense of Curry and Howard, to an expressive type system for
the probabilistic event lambda-calculus, a vehicle calculus in which both
call-by-name and call-by-value evaluation of discrete randomized functional
programs can be simulated. Remarkably, proofs (respectively, types) do not only
guarantee that validity (respectively, termination) holds, but also reveal the
underlying probability. We finally show that by endowing the type system with
an intersection operator, one obtains a system precisely capturing the
probabilistic behavior of lambda-terms.
