Curry-Howard Isomorphism (replies)

As requested here follows the list of replies I received on the
following request:

>> Can anyone refer me to material in which the CH-isomorphism for logics
>> with subtyping is studied? 
>> Your help is appreciated!

> From: Jakob Rehof <rehof@diku.dk>

There is a paper in LICS '95
by Longo, Milsted and Soloviev

  "A Logic of Subtyping (Extended Abstract)"

In this paper the authors say that

"... we propose a logical theory of
subtyping, as a fragment of intuitionistic
(linear) second order propositional calculus."

I guess they regard a subtyping statement
s \leq t as an intuitionistic implication,-
haven't read the details yet, though.
Note that their subtype system is a 
second order system, deriving, as I understand,
from Mitchell's paper "Polymorphic Type
Inference and Containment" (Inf. & Comp. 1988.)

> From: "C. Gunter" <C.Gunter@newton.cam.ac.uk>

An indirect form of CH correspondence for type systems with subtyping
could be derived from the `Penn translation'.  There are several
related articles in

editor = "C. A. Gunter and J. C. Mitchell",
title = "Theoretical Aspects of Object-Oriented Programming: Types, Semantics, \
and Language Design",
year = "1994",
publisher = "The {MIT} Press"}

See the one by Coquand et al if this suggestion interests you.

Thanks for the replies,

-- Dirk