
The functional paradigm of computation has been widely investigated and given a solid mathematical foundation, initiated with the CurryHoward isomorphism, then elaborated and extended in multiple ways. However, this paradigm is inadequate to capture many useful programming intuitions, arising in particular in the development of applications integrating distributed, autonomous components. Indeed, in this context, nondeterminism and true concurrency are the rule, whereas functional programming stresses determinism, and, although it allows some degree of concurrency, it is more as a "nice feature to have" rather than a primary assumption.
This paper is part of a program the ambition of which is to provide a logical foundation to a set of programming intuitions which, until now, have not been adequatly accounted for. In particular, we are interested in the intuitions which lie behind the concept of transaction, a powerful and essential concept in distributed componentbased application development. This concept is independent of the application domain and usually captured in an abstract form in middleware architectural layers.
We claim here that proofconstruction, and more precisely proofnet construction in Linear Logic, offers the adequate basis for our purpose. We outline the relation, which is of the same nature as the CurryHoward isomorphism, between transactional concepts and mechanisms on one hand, and proofnet construction on the other.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 