Dagger linear logic for categorical quantum mechanics