# A Probabilistic Dependent Type System based on Non-Deterministic Beta Reduction

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Feb 2016.

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

- [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)
- [Paraconsistent Foundations for Quantum Probability](https://mlsanity.com/paper/2101.07498/) (2021)

## Abstract (arXiv)

We introduce Probabilistic Dependent Type Systems (PDTS) via a functional language based on a subsystem of intuitionistic type theory including dependent sums and products, which is expanded to include stochastic functions. We provide a sampling-based semantics for the language based on non-deterministic beta reduction. Further, we derive a probabilistic logic from the PDTS introduced as a direct result of the Curry-Howard isomorphism. The probabilistic logic derived is shown to provide a universal representation for finite discrete distributions.