[PRL] Type question...

[Mitchell Wand]

On 10/5/07, Felix S Klock II <pnkfelix at ccs.neu.edu> wrote:
>
>
> On Oct 5, 2007, at 8:24 AM, Mitchell Wand wrote:
>
> > Just back from ICFP, so I'm only getting to this now.
> >
> > Of course Y (and its friends) have no simple type, because the
> > simply-typed lambda calculus is strongly normalizing, and Y has no
> > normal form.
> >
> > Every pure lambda term is typable with recursive types, since you
> > can give any pure lambda term the type  (mu t)(t -> t).  If you add
> > constants, of course, all bets are off.
> >
> > I believe there is a theorem that says that all pure lambda terms
> > are typable using intersection types, but I don't know the details.
>
> Mmm, I think the theorem is that a term is strongly normalizing if
> and only if it is typable using intersection types.
>
> -Felix


I stand corrected, sorry.  --Mitch
-------------- next part --------------
HTML attachment scrubbed and removed