Typing termination in a higher-order concurrent imperative language

We propose means to predict termination in a higher-order imperative and concurrent language a 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. (C) 2010 Elsevier Inc. All rights reserved.