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

Re: Coherence and polymorphic instantiation



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