[Prev][Next][Index][Thread]
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
entitled:
"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
@book{gunter-mitchell94,
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