Uniqueness logic
- 作者：Dana Harrington
- 关键词：Type systems ; Linear logic ; Functional programming ; Category theory ; Semantics
- 刊名：Theoretical Computer Science
- 出版年：2006
- 期刊代码：114_03043975
- 类别：cp
- 出版时间：21 March 2006
- 卷：354
- 期：1
- 页码：24-41
- 文件大小：249 K
摘要
A uniqueness type system is used to distinguish values which are referenced at most once from values which may be referenced an arbitrary number of times in a program. Uniqueness type systems are used in the Clean and Mercury programming languages to provide efficiently updatable data-structures and I/O without compromising referential transparency.
In this paper we establish a Curry–Howard–Lambek equivalence between a form of uniqueness types and a ‘resource-sensitive’ logic. This logic is similar to intuitionistic linear logic, however the modality, which moderates the structural rules in the antecedent in the same way as !, is introduced via the dual ? rules. We discuss the categorical proof theory and models of this new logic, as well as its computational interpretation.