Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System

Satoshi Kura, Hiroshi Unno

Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabi…