Filip Koprivec: Proving probabilistic programs correct
Abstract: I will describe my recent LFCS summer research internship with Dr. Ohad Kammar. The main goal of the internship was to migrate existing `koka-bayes` library to accommodate changes in koka 2.0 and devise a logic to reason about probabilistic programs.
I will present the development of Higher-order logic (HOL) for simple probabilistic programming language. HOL uses Quasi-Borel semantics to facilitate reasoning about higher-order probabilistic programs. HOL was extended to statistical program logic (SPL) to enable reasoning about distributions.
Using SPL, we can define Hoare triples to reason about the program and can be extended to various programming constructs (composition and conditionals). The resulting logic and rules enable us to reason about the probabilistic programs line by line and prove the correctness of the resulting distributions.
I will show a simple reasoning example on modified koka-like language and usage of effects to construct models that can be used in bayesian machine learning.
This is joint work with Ohad Kammar and Daan Leijen.
