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