# A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 21 references that are in the map.
- First posted on arXiv 30 Mar 2022.

## Builds on (most cited first, 7 of 7)

- [Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints](https://mlsanity.com/paper/1601.04943/) (2016)
- [Folding and Unfolding on Metagraphs](https://mlsanity.com/paper/2012.01759/) (2020)
- [Paraconsistent Foundations for Probabilistic Reasoning, Programming and Concept Formation](https://mlsanity.com/paper/2012.14474/) (2020)
- [Guarded Cubical Type Theory: Path Equality for Guarded Recursion](https://mlsanity.com/paper/1606.05223/) (2016)
- [Denotational semantics of recursive types in synthetic guarded domain theory](https://mlsanity.com/paper/1805.00289/) (2018)
- [Bisimulation as path type for guarded recursive types](https://mlsanity.com/paper/1810.13261/) (2018)
- [Reflective Metagraph Rewriting as a Foundation for an AGI "Language of Thought"](https://mlsanity.com/paper/2112.08272/) (2021)

## Abstract (arXiv)

We introduce a formal meta-language for probabilistic programming, capable of expressing both programs and the type systems in which they are embedded. We are motivated here by the desire to allow an AGI to learn not only relevant knowledge (programs/proofs), but also appropriate ways of reasoning (logics/type systems). We draw on the frameworks of cubical type theory and dependent typed metagraphs to formalize our approach. In doing so, we show that specific constructions within the meta-language can be related via bisimulation (implying path equivalence) to the type systems they correspond. This allows our approach to provide a convenient means of deriving synthetic denotational semantics for various type systems. Particularly, we derive bisimulations for pure type systems (PTS), and probabilistic dependent type systems (PDTS). We discuss further the relationship of PTS to non-well-founded set theory, and demonstrate the feasibility of our approach with an implementation of a bisimulation proof in a Guarded Cubical Type Theory type checker.