[PL-sem-jr] well-going programs can be typed

[Felix S Klock II]

All-

Here is one of the stranger papers I've seen since the Forsythe one:

http://www.cs.kent.ac.uk/pubs/2003/1649/

The abstract:
> Our idiomatically objectionable title is a pun on Milner's 
> ``well-typed programs do not go wrong' --- because we provide a 
> completeness result for type-checking rather than a soundness result.
>
>  We show that the well-behaved functions of untyped PCF are already 
> expressible in typed PCF: any equivalence class of the partial logical 
> equivalence generated from the flat natural numbers in the model given 
> by PCF's operational semantics is inhabited by a well-typed term.

Its got Scott's $D_{\infty}$, PCF, Retractions, PERs, Logical 
Relations, . . .

And yet the paper itself is 50% tricks with Haskell type classes and 
GHC extensions.

My current thinking is that the title is extremely misleading, but I 
won't go into why here.

-Still Sick Felix

p.s. do you all think that PRL, pl-seminar, or the CSG264 lists would 
have been more appropriate for this email?  Just curious.

----
WINDMILLS DO NOT WORK THAT WAY!  GOOD NIGHT!