Just to continue the academic nitpicking.. :-)
Linear logic/typing does not quite capture uniqueness types since a term with a unique type can always be copied to become non-unique, but a
Hello, linear
type cannot become unrestricted.
Actually, that isn't quite accurate. In linear logic, a term with a non-linear type can always be regarded as having a linear type, i.e.
U -o !U
is a theorem (my favourite reading of this theorem is "if you have an unlimited supply of bank notes, then you also have a single one"). The implication in the opposite direction is a falsity (from the fact that we have a single bank note, we cannot decude that we have an unlimited supply).
I think you mean !U -o U is a theorem. The converse is not provable. In any case, I think we are saying the same thing. -Jeff --- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.