That same function appears on the second page of Philip Wadler's first Linear Logic paper, but it's called "kill" [1]
But I remember the words "drop" and "dup" being used since the early days of linear logic too. I believe they come from Forth, where they do pretty much the same thing! [2]
But I remember the words "drop" and "dup" being used since the early days of linear logic too. I believe they come from Forth, where they do pretty much the same thing! [2]
[1] http://homepages.inf.ed.ac.uk/wadler/papers/linear/linear.ps
[2] http://wiki.laptop.org/go/Forth_stack_operators