A Formalized Hierarchy of Probabilistic System Types

DOI10.1007/978-3-319-22102-1_13zbMath1465.68199OpenAlexW1417233894MaRDI QIDQ2945633

Johannes Hölzl, Dmitriy Traytel, Andreas Lochbihler

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_13

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Formalization of mathematics in connection with theorem provers (68V20)

Related Items

Eisbach: a proof method language for Isabelle ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ Unnamed Item ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ Zoo Probabilistic Systems ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

Cites Work

• Unnamed Item
• A hierarchy of probabilistic system types
• Proofs of randomized algorithms in Coq
• Bisimulation through probabilistic testing
• Structural induction and coinduction in a fibrational setting
• Universal coalgebra: A theory of systems
• Bisimulation for probabilistic transition systems: A coalgebraic approach
• A Verified Compiler for Probability Density Functions
• Witnessing (Co)datatypes
• Truly Modular (Co)datatypes for Isabelle/HOL
• Cardinals in Isabelle/HOL
• Experience Implementing a Performant Category-Theory Library in Coq
• An Isabelle Proof Method Language
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Formalized Hierarchy of Probabilistic System Types
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Formal certification of code-based cryptographic proofs
• Probabilistic relational verification for cryptographic implementations
• Theorem Proving in Higher Order Logics
• Semantics of Probabilistic Processes