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

DOI10.1007/978-3-030-99461-7_4OpenAlexW4285158717MaRDI QIDQ2163157

Yasuhiko Minamide, Michikazu Hirata, 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 verificationprogram logicIsabelle/HOLhigher-order probabilistic programming language

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Notions of computation and monads
• Borel structures for function spaces
• Isabelle/HOL. A proof assistant for higher-order logic
• A formally verified proof of the central limit theorem
• Markov chains and Markov decision processes in Isabelle/HOL
• The HOL Light theory of Euclidean space
• Probabilistic guarded commands mechanized in HOL
• A Verified Compiler for Probability Density Functions
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Three Chapters of Measure Theory in Isabelle/HOL
• The Lean Theorem Prover (System Description)
• Proofs of Randomized Algorithms in Coq
• A Convenient Category for Higher-Order Probability Theory
• On the Formalization of the Lebesgue Integration Theory in HOL

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