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

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 ensur...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2004-05, Vol.51 (1), p.153-196
Main Authors: Backhouse, Kevin, Backhouse, Roland
Format: Article
Language:English
Subjects:
Abstract interpretation
Galois connections
Logical relations
Parametricity
Theorems for free
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2003.06.002