Le 8 mars 2010, à 13h30 en salle B311, Virgile Mogbil (LIPN) animera une séance du groupe de travail "Logique et Programmation".
We present a proofs-as-programs correspondence between linear logic and process calculi that handles non-deterministic behaviours. The proof language is that of wireless proof nets, i.e. multiplicative proof nets with sets of cut formulas instead of cut wires. A correspondence is established between proof structures and pi-calculus terms under an interfacing condition. Correctness criteria for proofs induce a type system for processes where typing a term consists in typing some of its possible determinisations in standard sequent calculus. Generalized cut-elimination in proof nets is shown to correspond to deadlock-avoiding execution. (With Emmanuel Beffara - IML)