On the Versatility of Open Logical Relations - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

On the Versatility of Open Logical Relations

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : hal-02991652 , version 1

Citer

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⟩
39 Consultations
151 Téléchargements

Partager

Gmail Facebook X LinkedIn More