Tutorial on Logical Relation and Relational Parametricity Seminars/Workshops

Abstract

July 11: Logical Relation for Abstract Interpretation
Abstract: In the mid 80's, one of the main issues in the theory of abstract interpretation was how to handle higher-order functions properly. While Cousot's original approach to design abstract domains with Galois connection is conceptually appealing, it has difficulties to handle higher-order functions. To see the difficulties, suppose that C and A be concrete and abstract interpretations of type t such that P(C) and A are related by Galois connection. Then, to handle functions of type t->t, we need to find a Galois connection between P(C->C) and A->A. However, the theory of Galois connection is silent for this question: even though P(C)->P(C) and A->A are Galois-connected, it is not clear whether the domains P(C->C) and A->A are Galois-connected when P is a powerset constructor "preserving" the order in C, i.e., a powerdomain constructor. In this tutorial, I will explain Abramsky's solution to this problem which uses logical relation instead of Galois connection. I will review what logical relation is, and why it has successfully been used to show difficult theorems, such as strong normalizability, for higher-order functions. Then, I will explain how Abramsky did abstract interpretation with abstract domains that are connected to concrete domains by logical relations.

July 12: An Introduction to Relational Parametricity
Abstract: Relational parametricity has proposed by Reynolds to explain in what sense parametric polymorphism is different from ad-hoc polymorphism or overlaoding. Intuitively, relational parametricity says that when a polymorphic term is applied to a type, it does not look at the type argument. To formalize "does not look at" part, Reynolds used relations, and interpreted type constructors, such as -> and X, as maps from relations to relations, following the interpretations in logical relation; then, he interpreted a polymorphic type, forall a.t(a), as type-indexed families of terms, such as {m_t' : t(t')}_{t' in type}, satisfying the parametricity condition: for all relations R:t0 <-> t1, m_t0 is related to m_t1 by [t](R), where [t] is a relational interpretation of a type-constructor. Reynolds showed that his condition is not so restrictive so that all polymorphic terms written in the system F satisfies the condition, and that for many types, the parametricity condition precisely captures the idea of "not looking at a type parameter"; for instance, the type, forall a.a->a, is interpreted as a singleton set only having an identity function. This talk is a review Reynolds' relational parametricity. I will also explain the use of relational parametricity in different contexts; relational parametricity has been used to explain the independence of a local variable from global procedures, and the independence of a secure information from attackers.

July 19: Heap Parametricity
Abstract: While relational parametricity was originally proposed to capture independence, Reynolds immediately noticed that it can also be used to explain data abstraction: if a client does not look at the internal representation of an abstract data type, the implementation of the data type can be changed without being noticed by a client as long as the external behavior remains unchanged. O'Hearn, Tennent, Reynolds and I myself have been doing research on this direction, and have found a reasonable semantic explanation for data abstraction of a higher-order imperative programming language with stack storage only. This talk is about how to extend such a result with heap storage. Heap storage raises many difficulties: the heap cells accessed by a program varies dramatically depending on which states the program starts, and the address of an heap cell is passed around (or leaked) so that it is difficult to guarantee that only an abstract data type manipulates certain heap cells. Our idea is to use spatial conjunction for relations in an RG-functor category semantics. Spatial conjunction for relations allows us to decide which heap cells belong to a client and which belong to an abstract data type in a input-state dependent manner, and the RG-functor category framework makes it easier to keep track of which heap cells have been leaked to a client (using a partial isomorphism as a part of edges). This is a joint ongoing work with Hongseok Yang.