[Prev][Next][Index][Thread]
Re: Coherence and polymorphic instantiation
-
To: types
-
Subject: Re: Coherence and polymorphic instantiation
-
From: ma@src.dec.com (Martin Abadi)
-
Date: Wed, 05 Aug 92 10:36:43 EDT
-
In-Reply-To: Message of Tue, 04 Aug 92 09:03:23 EDT from Benjamin Pierce <bcp@dcs.ed.ac.uk> <199208041303.AA24220@stork.lcs.mit.edu>
-
Sender: meyer@theory.lcs.mit.edu
Date: Tue, 4 Aug 92 13:32:53 PDT
This issue can be considered in Fsub, as Andre points out, but it
already arises in F. John Mitchell studied the theories where
any two terms with the same type and the same erasure are equated;
he proved that any such theory corresponds to some PER model. (See
p. 208 in "Logical Foundations of Functional Programming", ed. Huet.)
Martin Abadi