Lambda the Ultimate

I found it odd that we hadn't mentioned this paper before on LtU (that or my Google-fu has failed me).

I think this is a quite interesting basis from which to go beyond the static vs. dynamic debate and think interesting thoughts about static and dynamic living together in harmony (except for some bouts of blaming each other that all good friends are bound to have on occasion. ;-) )

Hopefully it won't be too controversial (!) for me to add that my interest in this topic was sparked by the growing feeling that we are starting to bump up against the limits of what can sensibly be done with homogeneous, pure static type systems (both theoretically and practically), and that the direction for future work may depend on finding ways to get different type systems or different degrees of typing to play well together.