headers
Eijiro Sumii | 4 Aug 2006 05:18
Picon

[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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Dimitrios Vytiniotis | 22 Aug 2006 00:19
Favicon

logical relations and ctx equivalence

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

Dear TYPES readers,

    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
(Continue reading)

Permalink | Reply | 0 comments |

Gmane