An affine-intuitionistic system of types and effects: confluence and termination

Clinical Orthopaedics and Related Research(2010)

引用 23|浏览5
暂无评分
摘要
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.
更多
查看译文
关键词
system dynamics,stratification,linear logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要