Divergences on Monads for Relational Program Logics

TL;DR

This paper introduces a general relational program logic, acRL, that formalizes divergences on monads to reason about relational properties and quantitative differences in computational effects, with applications in differential privacy and cost analysis.

Contribution

It develops a categorical framework for divergences on monads and derives a generic logic supporting various computational effects and divergences.

Findings

Successfully instantiated acRL for differential privacy verification.

Applied acRL to analyze cost differences in probabilistic programs.

Provided a categorical semantics for divergences on monads.

Abstract

Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computational effects. Towards a general framework for such logics, in this paper, we formalize quantitative difference between computational effects as divergence on monad, then develop a relational program logic acRL that supports generic computational effects and divergences on them. To give a categorical semantics of acRL supporting divergences, we give a method to obtain graded strong relational liftings from divergences on monads. We derive two instantiations of acRL for the verification of 1) various differential privacy of higher-order functional probabilistic programs and 2) difference of distribution of costs between higher-order functional programs with probabilistic choice and cost counting operations.