[Prev][Next][Index][Thread]
Re: logical relations and soundness of type systems ?
Hans Huttel wrote:
> Can the notion of logical relations be used to prove the soundness of
> type systems or is our naiveti 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.
>
Proofs of type soundness sometimes do use this technique but without
explicit mention of the term "logical relation". For example (picking a
paper more or less at random), the article "Unboxed objects and
polymorphic typing" by Xavier Leroy in POPL'92 proves semantic
correctness of a typed translation by means of a relation which is
essentially `logical': at functional type it relates functions for which
"related arguments yield related results". Leroy in turn cites Milner
and Tofte's "Type inference for polymorphic references" from Information
and Computation, 89(1), 1990. I'm sure there are many more examples.
-- Andrew.
--------------------------------------------------------------------
Dr Andrew Kennedy phone:
Research Scientist +44 1223 578770
Persimmon IT
1st floor, Block C email:
The Westbrook Centre Andrew.Kennedy@persimmon.co.uk
Milton Road
Cambridge, CB4 1YG, UK
--------------------------------------------------------------------