# On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem

arXiv: https://arxiv.org/abs/2002.08489 · HTML: https://mlsanity.com/paper/2002.08489/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Feb 2020.

## Built on by (most cited first, 5 of 5)

- [Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference](https://mlsanity.com/paper/2208.10530/) (2022)
- [On the Correctness of Automatic Differentiation for Neural Networks with Machine-Representable Parameters](https://mlsanity.com/paper/2301.13370/) (2023)
- [Efficient and Sound Differentiable Programming in a Functional Array-Processing Language](https://mlsanity.com/paper/2212.10307/) (2022)
- [GradInf: Gradient Estimation as Probabilistic Inference](https://mlsanity.com/paper/2607.07840/) (2026)
- [LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs](https://mlsanity.com/paper/2608.08588/) (2026)

## Abstract (arXiv)

Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we study a generalization of the concept of a logical relation, called open logical relation, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed λ-calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any such a collection of functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations.