4 Aug 2006 05:18

### [TYPES/announce] Call for Posters, APLAS 2006 (in Sydney, in November)

```[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

CALL FOR POSTER PRESENTATIONS

The Fourth ASIAN Symposium on Programming Languages and Systems
(APLAS 2006)

November 8-10, 2006
University of New South Wales, Sydney, Australia

Deadline for Abstracts: September 11, 2006

APLAS 2006 will include a poster session during the conference.  The
session aims to give students and researchers an opportunity to
present their research to the community, and to get responses from
other researchers.

SCOPE:

Poster presentations are sought in all areas of programming languages
and systems, including (but not limited to):

- semantics, logics, foundational theory
- type systems, language design
- program analysis, optimization, transformation
- software security, safety, verification
- compiler systems, interpreters, abstract machines
- domain-specific languages and systems
- programming tools and environments
```

22 Aug 2006 00:19

### logical relations and ctx equivalence

```[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Consider the simplest syntactic relational interpretation of
System-F types as sets of pairs of closed values.  Quantification is
over arbitrary value relations. The semantics is call by value and
terminating. [Definitions can be found at the end of this message]

First, I think it is an easy corollary of the fundamental theorem that
the logical relation is contained in ctx equivalence (I am using
ground equivalence, actually), i.e. that:

Proposition: If (e1,e2) in (interp[t] nil nil)
then forall contexts C : t -> Int,
C[e1] and C[e2] evaluate to the same literal.

What I am asking is whether we know that it is complete:

Question: If forall C : t -> Int,
C[e1] and C[e2] evaluate to the same literal
then (e1,e2) in (interp[t] nil nil).

It seems that an important step towards completeness is showing that
the logical relation is an equivalence-respecting one. Then, for
example, Pitts' work [ATTAPL clapter] uses TT-closures, and Harper &
Birkedal's paper [Relational interpetation for recursive types in an
Operational Setting] builds the logical relation between equivalence
classes of expressions alltogether (and does not handle polymorphism,
but this probably does not matter). Are all these constructions
```