Program logic for higher-order probabilistic programs in Isabelle/HOL

DOI10.1007/978-3-030-99461-7_4MaRDI QIDQ2163157zbMATH OpenOpenAlexFDO

Authors Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato

Publication date 10 August 2022

Full work available at URL https://doi.org/10.1007/978-3-030-99461-7_4

zbMATH Keywords

formal verificationhigher-order probabilistic programming languageIsabelle/HOLprogram logic

Mathematics Subject Classification ID

Logic programming (68N17) Functional programming and lambda calculus (68N18)

Recommendations

• A Convenient Category for Higher-Order Probability Theory
• VPHL: a verified partial-correctness logic for probabilistic programs
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• scientific article; zbMATH DE number 1500556
• Verification of Probabilistic Programs

Cites work

• A Convenient Category for Higher-Order Probability Theory
• A formally verified proof of the central limit theorem
• A verified compiler for probability density functions
• Borel structures for function spaces
• scientific article; zbMATH DE number 3764843 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Markov chains and Markov decision processes in Isabelle/HOL
• Notions of computation and monads
• On the formalization of the Lebesgue integration theory in HOL
• Probabilistic functions and cryptographic oracles in higher order logic
• Probabilistic guarded commands mechanized in HOL
• Proofs of Randomized Algorithms in Coq
• The HOL Light theory of Euclidean space
• The Lean theorem prover (system description)
• Three chapters of measure theory in Isabelle/HOL

Cited in

(4)

• An assertion-based program logic for probabilistic programs
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• scientific article; zbMATH DE number 1500556 (Why is no real title available?)
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving

Describes a project that uses

Uses Software

• mathlib
• ML
• pGCL
• Coq
• PVS
• HOL
• Lean
• Church
• Quasi-Borel Spaces
• Isabelle/HOL
• Transfer
• Lifting
• Archive of Formal Proofs
• Density Compiler

This page was built for publication: Program logic for higher-order probabilistic programs in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2163157)