[Prev][Next][Index][Thread]

logical relations and soundness of type systems ?


This is a naive question about logical relations in the context of the
object calculi due to Abadi and Cardelli.

In [1] we study the relationship between the type system and a modal
logic of objects. A main result is that there exists a translation
function T from types in the type system Ob1mu< to formulae in the
modal mu-calculus such that

If the object o has type A then o satisfies the modal formula T(A)

Here, the satisfiability of a modal formula is defined inductively
relative to a labelled transition semantics of objects.

This is essentially a result on type soundness. Now we (Josva Kleist
and I) would now like to prove the theorem anew using some notion of
logical relation suitably adapted to the world of the object calculus.

Can the notion of logical relations be used to prove the soundness of
type systems or is our naiveté showing ? (In the literature that we
have come across on logical relations for typed lambda calculi, we
have not seen any actual references to proofs of soundness of type
systems w.r.t. a model of types that use logical relations but logical
relations are useful in many other related situations.)

Pointers to literature/suggestions will be much appreciated.

References
----------

[1] Andersen, Hostrup, Hüttel, Kleist: Object Types as Modal Formulae,
Proc. of FOOL4, Paris 1997.

--
Hans Huttel,  office E1-111              | hans@cs.auc.dk
BRICS, Dept. of Computer Science         | fax: (+45) 98 15 98 89
Aalborg University, Fredrik Bajersvej 7E | tel.: (+45) 96 35 88 88
9220 Aalborg \emptyset, DENMARK.         | WWW: http://www.cs.auc.dk/~hans/