On stratified regions
Logic in Computer Science
2010-07-01 v2
Abstract
Type and effect systems are a tool to analyse statically the behaviour of programs with effects. We present a proof based on the so called reducibility candidates that a suitable stratification of the type and effect system entails the termination of the typable programs. The proof technique covers a simply typed, multi-threaded, call-by-value lambda-calculus, equipped with a variety of scheduling (preemptive, cooperative) and interaction mechanisms (references, channels, signals).
Cite
@article{arxiv.0904.2076,
title = {On stratified regions},
author = {Roberto Amadio},
journal= {arXiv preprint arXiv:0904.2076},
year = {2010}
}