Typing termination in a higher-order concurrent imperative language

We propose means to predict termination in a higher-order imperative and concurrent language à la ML. 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 establish that typable sequential programs in our system are guaranteed to terminate, unless they use explicit recursion in a divergent way. We actually prove a more general fairness property, that is, any typable thread yields the scheduler after some finite computation. Our realizability interpretation also copes with dynamic thread creation.