Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to handle the quantitative aspects of probabilistic programs often entails extensive modifications to existing tools, reducing compatibility with advanced techniques developed for qualitative verification. In contrast, our approach necessitates only small amounts of modification, facilitating the reuse of existing techniques and implementations. On the theoretical side, we propose a dependent refinement type system for a generalised higher-order fixed point logic (HFL). Combined with continuation-passing style encodings of properties into HFL, our dependent refinement type system enables reasoning about several quantitative properties, including weakest pre-expectations, expected costs, moments of cost, and conditional weakest pre-expectations for higher-order probabilistic programs with continuous distributions and conditioning. The soundness of our approach is proved in a general setting using a framework of categorical semantics so that we don't have to repeat similar proofs for each individual problem. On the empirical side, we implement a type checker for our dependent refinement type system that reduces the problem of type checking to constraint solving. We introduce admissible predicate variables and integrable predicate variables to constrained Horn clauses (CHC) so that we can soundly reason about the least fixed points and samplings from probability distributions. Our implementation demonstrates that existing CHC solvers developed for non-probabilistic programs can be extended to a solver for the extended CHC with only small efforts. We also demonstrate the ability of our type checker to verify various concrete examples.

翻译：高阶概率程序的验证是一个具有挑战性的问题。我们提出了一种验证方法，支持高阶概率程序的多种定量性质。通常，将验证方法扩展以处理概率程序的定量方面，往往需要对现有工具进行大量修改，从而降低了与为定性验证开发的先进技术的兼容性。相比之下，我们的方法仅需少量修改，便于复用现有技术和实现。在理论方面，我们为广义高阶不动点逻辑（HFL）提出了一种依赖精化类型系统。结合将性质通过续传风格编码到HFL中，我们的依赖精化类型系统能够对具有连续分布和条件化的高阶概率程序的多种定量性质进行推理，包括最弱前置期望、期望代价、代价矩以及条件最弱前置期望。我们方法的可靠性在一个通用设置下，利用范畴语义框架得以证明，从而无需为每个具体问题重复类似的证明。在实证方面，我们为我们的依赖精化类型系统实现了一个类型检查器，将类型检查问题约简为约束求解。我们为约束霍恩子句（CHC）引入了可容许谓词变量和可积谓词变量，从而能够可靠地推理最小不动点以及从概率分布中的采样。我们的实现表明，为无概率程序开发的现有CHC求解器只需付出少量努力即可扩展为适用于扩展CHC的求解器。我们还展示了我们的类型检查器验证各种具体示例的能力。