On the Versatility of Open Logical Relations - Archive ouverte HAL Access content directly
Conference Papers Year :

On the Versatility of Open Logical Relations

(1) , (2) , (3, 4) , (3, 2, 4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
main.pdf (481.32 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02991652 , version 1 (06-11-2020)

Identifiers

  • HAL Id : hal-02991652 , version 1

Cite

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⟩
33 View
111 Download

Share

Gmail Facebook Twitter LinkedIn More