An affine-intuitionistic system of types and effects: confluence and termination
Logic in Computer Science
2009-12-03 v1
Abstract
We present an affine-intuitionistic system of types and effects which can be regarded as an extension of Barber-Plotkin Dual Intuitionistic Linear Logic to multi-threaded programs with effects. In the system, dynamically generated values such as references or channels are abstracted into a finite set of regions. We introduce a discipline of region usage that entails the confluence (and hence determinacy) of the typable programs. Further, we show that a discipline of region stratification guarantees termination.
Keywords
Cite
@article{arxiv.0912.0419,
title = {An affine-intuitionistic system of types and effects: confluence and termination},
author = {Roberto Amadio and Patrick Baillot and Antoine Madet},
journal= {arXiv preprint arXiv:0912.0419},
year = {2009}
}