Skip to Main content Skip to Navigation
Conference papers

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

Abstract : Logical relations are one among 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 differen-tiability 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 collection of real-valued first-order 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 con-ditionals, and prove the soundness of the type system using open logical relations.
Document type :
Conference papers
Complete list of metadata

Cited literature [59 references]  Display  Hide  Download
Contributor : Francesco Gavazzo Connect in order to contact the contributor
Submitted on : Friday, November 6, 2020 - 9:55:22 AM
Last modification on : Friday, July 9, 2021 - 5:18:01 PM
Long-term archiving on: : Sunday, February 7, 2021 - 6:24:48 PM


Files produced by the author(s)


  • HAL Id : hal-02991652, version 1



Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo. On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem. ESOP 2020 - 29th European Symposium on Programming. Held as Part of the ETAPS 2020 - European Joint Conferences on Theory and Practice of Software, Apr 2020, Dublin, Ireland. ⟨hal-02991652⟩



Record views


Files downloads