Curry-Howard pour la concurrence – CHOCO

The Curry-Howard correspondence, which relates mathematical proofs to computer programs, is a very powerful paradigm which, for the time being, is retricted to purely "sequential" programming languages. We plan to extend this paradigm to the concurrent languages described by process algebras such as the pi-calculus. For this purpose, we shall use the recently established connexions between differential interaction nets (an extension of linear logic) and process algebras. We shall also take benefit from the recently discovered connexions between causal semantics of process algebras and game theoretic models of linear logic. We shall use this work for defining new and logically grounded process algebras, for which we shall define a realizability theory which will recast in a more convincing proof-theoretic setting the spatial and temporal logics used for specifying the behavior or processus.