Interesting resource. Given that "no-cloning" [1] seems to be a fundamental property of quantum mechanics, I would expect any relevant programming language to enforce linear types i.e. "use exactly once" constraint. [1]: https://quantiki.org/wiki/no-cloning-theorem
The linked paper says in the abstract: The calculus turns out to be closely related to the linear lambda calculi used in the study of Linear Logic. We set up a computational model and an equational proof system for this calculus, and we argue that it is equivalent to the quantum Turing machine.
Yes, I was placing that statement in context.