Lambda the Ultimate

Fair cooperative multithreading, or: Typing termination in a higher-order concurrent imperative language. September 2007. A preliminary version (without proofs, recursion and region-scoping) appeared in the proceedings of CONCUR'07, LNCS 4703 (2007), 272-286.

We propose a new operational model for shared variable concurrency, in
the context of a concurrent, higher-order imperative language à la ML.
In our model the scheduling of threads is cooperative, and a
non-terminating process suspends itself on each recursive call. A
property to ensure in such a model is fairness, that is, any thread
should yield the scheduler after some finite computation. To this end,
we follow and adapt the classical method for proving termination in
typed formalisms, namely the realizability technique. There is a
specific difficulty with higher-order state, which is that one cannot
define a realizability interpretation simply by induction on types,
because applying a function may have side-effects at types not smaller
than the type of the function. Moreover, such higher-order side-effects
may give rise to computations that diverge without resorting to explicit
recursion. We overcome these difficulties by introducing a type and
effect system for our language that enforces a stratification of the
memory. The stratification prevents the circularities in the memory that
may cause divergence, and allows us to define a realizability
interpretation of the types and effects, which we then use to prove the
intended termination property. Our realizability interpretation also
copes with dynamic thread creation.

Slides are available, not just the paper, and provide a nice introduction to approaches for proving termination, which may be useful in their own right to those not familiar with the topic.