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

Jonathan H. Warrell

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1602.06420 v2 pith:YZMIXRAD submitted 2016-02-20 cs.LO cs.PL

Jonathan H. Warrell This is my paper

classification cs.LOcs.PL

keywords probabilisticdependenttypebetalanguagelogicnon-deterministicpdts

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original abstract

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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Trustworthiness Preservation by Copies of Machine Learning Systems
cs.LO 2025-06 conditional novelty 5.0 of 10

A new typed natural deduction calculus defines four grades of trustworthiness for copies of ML systems and proves preservation under logical query composition.

Pith tools