logical relations and contextual equivalence

To: types@cis.upenn.edu
Subject: logical relations and contextual equivalence
From: Eijiro Sumii <sumii@saul.cis.upenn.edu>
Date: Wed, 21 Feb 2001 11:22:16 -0500
cc: sumii@saul.cis.upenn.edu

I am looking for (in)completeness results of logical relations
w.r.t. contextual equivalence---that is, whether contextually
equivalent terms can always be logically related---in typed
lambda-calculi.

In particular, I am interested in such results in the following
settings:

- with universal types or existential types
- with divergence or without divergence
- under call-by-name or call-by-value evaluation

My understanding is that logical relations are

- complete in a call-by-name setting with divergence and universal types
- incomplete in call-by-value settings with existential types
- incomplete in call-by-value settings with universal types

but corrections and any other information are _very_ welcome.

Thank you in advance,

// Eijiro Sumii (http://www.yl.is.s.u-tokyo.ac.jp/~sumii/)
// 
// Ph.D. Student at Department of IS, University of Tokyo
// Visiting Scholar at Department of CIS, University of Pennsylvania