Curry and Howard Meet Borel

We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expres- sive type system for the probabilistic event λ-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but reveal the underlying proba- bility. We finally show how to obtain a system precisely capturing the probabilistic behavior of λ-terms, by endowing the type system with an intersection operator.