Curry and Howard Meet Borel

TL;DR

This paper establishes a connection between an intuitionistic counting logic and a probabilistic lambda-calculus, introducing a type system that reveals probabilities and captures probabilistic behavior of programs.

Contribution

It introduces an expressive type system for probabilistic lambda-calculus that encodes probabilities and extends to capture probabilistic behavior with intersection types.

Findings

Type system reveals underlying probabilities of programs

Proofs guarantee validity and reveal probabilities

Extension with intersection types captures full probabilistic behavior

Abstract

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.