  There was a PhD student who says "I found a pair of wooden shoes. I put a
coin in the left and a key in the right. Next morning, I found those objects in
the opposite shoes." We do not claim existence of such shoes, but propose a
similar programming abstraction in the context of typed lambda calculi. The
result, which we call the Amida calculus, extends Abramsky's linear lambda
calculus LF and characterizes Abelian logic.
