Uniqueness logic

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.