Re: Coherence and polymorphic instantiation

Article View: fj.mail-lists.types

Article #6

Back to fj.mail-lists.types Previous Next

From: Martin Abadi
Date: Wed, 05 Aug 1992 16:09

9 lines
759 bytes

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

Technical Details

Message-ID: <313024@nttlab.ntt.JP>

Path: arc1-ca.pugleaf.net!sparky!uunet!sun-barr!sh.wide!wnoc-snd-ss2!akiu!hakata!kyu-cs!lab!nttlab!daemon

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!sparky!uunet!sun-barr!sh.wide!wnoc-snd-ss2!akiu!hakata!kyu-cs!lab!nttlab!daemon
From: ma@src.dec.com (Martin Abadi)
Newsgroups: fj.mail-lists.types
Subject: Re: Coherence and polymorphic instantiation
Message-ID: <313024@nttlab.ntt.JP>
Date: 5 Aug 92 16:09:37 GMT
Sender: daemon@nttlab.ntt.JP
Distribution: fj
Lines: 9
Approved: news@nttlab.ntt