Synthetic topology in Homotopy Type Theory for probabilistic programming

DOI10.1017/S0960129521000165MaRDI QIDQ5055499

Bas Spitters, Florian Faissole, Martin E. Bidlingmaier

Publication date: 9 December 2022

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1912.07339

zbMATH Keywords

topologyhomotopy type theoryprobabilistic programmingcategorical semantics

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

Commutative Semantics for Probabilistic Programming

Uses Software

• HoTT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A constructive manifestation of the Kleene-Kreisel continuous functionals
• Notions of computation and monads
• Metric Boolean algebras and constructive measure theory
• Quotient inductive-inductive types
• Continuous Truth II: Reflections
• Partiality, Revisited
• Type classes for mathematics in type theory
• Proofs of Randomized Algorithms in Coq
• Integrals and valuations
• On choice sequences determined by spreads
• On a Topological Topos
• Semantics for probabilistic programming
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• On Church’s thesis in cubical assemblies
• Partial Elements and Recursion via Dominances in Univalent Type Theory.
• A Convenient Category for Higher-Order Probability Theory
• Application ofComputable Distributions to the Semantics of Probabilistic Programs
• A Convenient Method for Generating Normal Variables
• Presenting Dcpos and Dcpo Algebras
• Homotopy Type Theory: Univalent Foundations of Mathematics
• A localic theory of lower and upper integrals
• Sets in homotopy type theory
• Measures in Boolean Algebras

This page was built for publication: Synthetic topology in Homotopy Type Theory for probabilistic programming