# A Type Theory for Probabilistic and Bayesian Reasoning

arXiv: https://arxiv.org/abs/1511.09230 · HTML: https://mlsanity.com/paper/1511.09230/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Nov 2015.

## Built on by (most cited first, 2 of 2)

- [Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System](https://mlsanity.com/paper/2206.12934/) (2022)
- [Trustworthiness Preservation by Copies of Machine Learning Systems](https://mlsanity.com/paper/2506.05203/) (2025)

## Abstract (arXiv)

This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.