Abstract:
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.