Session Types in Abelian Logic

Yoichi Hirai
(National Institute of Advanced Industrial Science and Technology)

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.

In Nobuko Yoshida and Wim Vanderbauwhede: Proceedings 5th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2013), Rome, Italy, 23rd March 2013, Electronic Proceedings in Theoretical Computer Science 137, pp. 33–52.
Published: 8th December 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: