Skip to main content
PRL Project

Randomized Programming and Probabilistic Reasoning in Type Theory

by James Cheney


Randomness and probability are core concepts in computer science, used in randomized algorithms, average case analyses of deterministic algorithms, and decision-making systems in AI. We want to incorporate random computations and probabilistic reasoning into NuPRL, for example to analyze and verify randomized gossip for Ensemble. However, there are some basic conflicts between the usual notions of probability and randomness that keep this from being striaghtforward. I'll present a number of approaches to doing probability in NuPRL and discuss their merits and drawbacks.

This is work in progress and I don't have all the answers. I plan to leave time at the end for discussion. I'd especially like to find out whether my approach sounds OK to the people working with Ensemble, or if not what should change.