Jean-Marc Andreoli, Laurent Mazaré
Computer Science Logic Conference, Vienna, Austria, August 25-30, 2003
The functional paradigm of computation has been widely investigated and given a solid mathematical
foundation, initiated with the Curry-Howard isomorphism, then elaborated and extended in multiple ways.
However, this paradigm is inadequqte to capture many useful programming intuitions, arising in particular in
the development of applications integrating distributed, autonomous components. Indeed, in this context,
on-determinism 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
component-based application development. This concept is independent of the application domain and usually
captured in an abstract form in middleware architecture layers. We claim here that proof-construction, and
more precisely proof-net construction in linear logic, offers the adequate basis for our purpose. We outline the
relation,which is of the same nature as the Curry-Howard isomorphism, between transactional concepts and
mechanisms on one hand, and proof-net cosntruction on the other.
Report number: