Back to Search
Start Over
Typing termination in a higher-order concurrent imperative language
- Source :
-
Information & Computation . Jun2010, Vol. 208 Issue 6, p716-736. 21p. - Publication Year :
- 2010
-
Abstract
- Abstract: 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. [Copyright &y& Elsevier]
Details
- Language :
- English
- ISSN :
- 08905401
- Volume :
- 208
- Issue :
- 6
- Database :
- Academic Search Index
- Journal :
- Information & Computation
- Publication Type :
- Academic Journal
- Accession number :
- 50734146
- Full Text :
- https://doi.org/10.1016/j.ic.2009.06.007