Encoding proofs with an interaction calculus

The relevance of typed $\lambda$-calculus in the study of the proofs is well known; the development of the \textsl{linear logic} has stimulated the interest in non functional systems. The calculus described in this paper was originally designed by the author to deal with the proofs of \textsl{linear logic}. The \textit{interaction calculus} is an evolution of the original one; it provides a natural environment for the study of of the proofs based on the concept of sequent. We basically deal with structured entities that represent processes or collection of processes sharing an environment; each process can be possibly connected with some others by means of variables. The computations are started up by the interaction between processes; the progress of the computation modifies the interacting entities and can eventually produce side-effects by means of a substitution. The interaction calculus is essentially non functional: that is processes cannot be commonly recognized as functions; in addition the calculus in the general case is not confluent. Even so $\lambda$-calculus is nicely represented in it and proofs of an intuitionist deductive system can smoothly be modelled. The symmetry and non functional nature of interaction, and a little more, yield a satisfactory framework in which we can handle proofs of linear or classical logic. We propose here the case of classical logic as a starting point for an investigation on the constructive features of its proofs.