Logical Relations for Monadic Types

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.

83 pages

Cited by in corpus (14)

• Towards 3-Dimensional Rewriting Theory
• Bimonoidal Structure of Probability Monads
• The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time
• On Probabilistic Applicative Bisimulation and Call-by-Value $\lambda$-Calculi (Long Version)
• Relational Parametricity for Computational Effects
• Bialgebraic Reasoning on Higher-Order Program Equivalence
• Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)
• Program Equivalence in Linear Contexts
• Extending Equational Monadic Reasoning with Monad Transformers
• The Quantum Monadology
• Codensity Lifting of Monads and its Dual
• A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential
• Logic of computational semi-effects and categorical gluing for equivariant functors
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules