[Prev][Next][Index][Thread]
Re: Decidable polymorphic recursion?
Josef Svenningsson
>> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>>
>> Hi!
>>
>> Does anybody know of any work on type systems which are somewhere in
>> between the Damas-Milner and the Milner-Mycroft calculus in strength? What
>> I am looking for is a type system for which we can infer the types but
>> still gives some kind of (but of course not full) polymorphic recursion.
>> Any pointers appreciated.
>>
>> /Josef
>>
You might have a look to the paper by P. Cousot in POPL'97. Type
systems are obtained by abstract interpretation of a detotational
semantics with dynamic types. In particular, the Damas-Milner is
derived from the Milner-Mycroft typing by a widening operation
after one fixpoint iteration. Other widenings are also suggested.
A full range of type systems between the two can be obtained
just by changing this wideing operation.
Best regards,
Radhia
--
Radhia COUSOT
CNRS & Ecole Polytechnique tel: +33 1 69 33 45 95
Laboratoire d'informatique (LIX) fax: +33 1 69 33 30 14
91128 Palaiseau cedex (France) Radhia.Cousot@polytechnique.fr