The Next 700 Relational Program Logics

TL;DR

This paper introduces a highly expressive, generic framework for defining relational program logics for various monadic effects, enabling formal reasoning about complex computational effects in a unified manner.

Contribution

It presents the first algebraic, effect-agnostic framework for relational program logics, capable of handling diverse effects including state, nondeterminism, probabilities, and exceptions.

Findings

Framework can define relational logics for multiple effects

Embedded a variant of Benton's Relational Hoare Logic

Provided the first relational logic for exceptions

Abstract

We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic presentation of relational specifications as a class of relative monads, and link computations and specifications by introducing relational effect observations, which map pairs of monadic computations to relational specifications in a way that respects the algebraic structure. For an arbitrary relational effect observation, we generically define the core of a sound relational program logic, and explain how to complete it to a full-fledged logic for the monadic effect at hand. We show that this generic framework can be used to define relational program logics for effects as diverse as state, input-output, nondeterminism, and discrete probabilities. We, moreover, show that by instantiating our framework with state and unbounded iteration we can embed a variant of Benton's Relational Hoare Logic, and also sketch how to reconstruct Relational Hoare Type Theory. Finally, we identify and overcome conceptual challenges that prevented previous relational program logics from properly dealing with control effects, and are the first to provide a relational program logic for exceptions.