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.
Thomas EHRHARD (Organisme de recherche)
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
Help of the ANR 277,000 euros
Beginning and duration of the scientific project: - 36 Months