Uniqueness logic

Citations of this article
Mendeley users who have this article in their library.


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. © 2005 Elsevier B.V. All rights reserved.




Harrington, D. (2006). Uniqueness logic. In Theoretical Computer Science (Vol. 354, pp. 24–41). https://doi.org/10.1016/j.tcs.2005.11.006

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free