Safety of abstract interpretations for free, via logical relations and Galois connections

被引：9
|
作者：
Backhouse, K [1 ]
Backhouse, R
机构：
[1] ARM Ltd, Cambridge CB1 9NJ, England
[2] Univ Nottingham, Sch Comp Sci & Informat Technol, Nottingham NG8 1BB, England
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2004年 / 51卷 / 1-2期
关键词：
abstract interpretation; logical relations; parametricity; theorems for free; Galois connections;
D O I：
10.1016/j.scico.2003.06.002
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Algebraic properties of logical relations on partially ordered sets are studied. It is shown how to construct a logical relation that extends a collection of base Galois connections to a Galois connection of arbitrary higher-order type. "Theorems-for-free" is used to show that the construction ensures safe abstract interpretation of parametrically polymorphic functions. The properties are used to show how abstract interpretations of program libraries can be constructed. (C) 2004 Elsevier B.V. All rights reserved.
引用
收藏
页码：153 / 196
页数：44
相关论文
共 50 条
  • [1] Logical relations and galois connections
    Backhouse, K
    Backhouse, R
    [J]. MATHEMATICS OF PROGRAM CONSTRUCTION, 2002, 2386 : 23 - 39
  • [2] Extracting Program Logics From Abstract Interpretations Defined by Logical Relations
    Schmidt, David A.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 173 : 339 - 356
  • [3] Logical Abstract Domains and Interpretations
    Cousot, Patrick
    Cousot, Radhia
    Mauborgne, Laurent
    [J]. FUTURE OF SOFTWARE ENGINEERING, 2011, : 48 - 71
  • [4] Biclosed Binary Relations and Galois Connections
    Florent Domenach
    Bruno Leclerc
    [J]. Order, 2001, 18 : 89 - 104
  • [5] Biclosed binary relations and Galois connections
    Domenach, F
    Leclerc, B
    [J]. ORDER-A JOURNAL ON THE THEORY OF ORDERED SETS AND ITS APPLICATIONS, 2001, 18 (01): : 89 - 104
  • [6] Logical relations for encryption (extended abstract)
    Sumii, E
    Pierce, BC
    [J]. 14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, : 256 - 269
  • [7] Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations
    Kammar, Ohad
    Katsumata, Shin-ya
    Saville, Philip
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6
  • [8] Deriving Logical Relations from Interpretations of Predicate Logic
    Hermida, Claudio
    Reddy, Uday S.
    Robinson, Edmund P.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2019, 347 : 241 - 259
  • [9] Transport via Partial Galois Connections and Equivalences
    Kappelmann, Kevin
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2023, 2023, 14405 : 225 - 245
  • [10] Abstract Effects and Proof-Relevant Logical Relations
    Benton, Nick
    Hofmann, Martin
    Nigam, Vivek
    [J]. ACM SIGPLAN NOTICES, 2014, 49 (01) : 619 - 631
12345