Logical Relations for Monadic Types

TL;DR

This paper develops a categorical framework for logical relations tailored to monadic types in lambda-calculi, enabling proofs of properties like observational equivalence across various computational effects.

Contribution

It introduces a novel categorical notion of logical relations for monadic types, extending their applicability to non-determinism, dynamic name creation, and probabilistic systems.

Findings

Logical relations can be adapted to monadic types in lambda-calculi.

The approach applies to non-deterministic and probabilistic systems.

It provides a foundation for reasoning about observational equivalence.

Abstract

Logical relations and their generalizations are a fundamental tool in proving properties of lambda-calculi, e.g., yielding sound principles for observational equivalence. We propose a natural notion of logical relations able to deal with the monadic types of Moggi's computational lambda-calculus. The treatment is categorical, and is based on notions of subsconing, mono factorization systems, and monad morphisms. Our approach has a number of interesting applications, including cases for lambda-calculi with non-determinism (where being in logical relation means being bisimilar), dynamic name creation, and probabilistic systems.