π-calculus, Session Types research at Imperial College

This paper presents an exact correspondence in typing and dynamics between polarised linear logic and a typed π-calculus based on IO-typing. The respective incremental constraints, one on geometric structures of proof-nets and one based on types, precisely correspond to each other, leading to the exact correspondence of the respective formalisms as they appear in Olivier Laurent (2003) 27 (for proof-nets) and Kohei Honda et al. (2004) 24 (for the π-calculus).

@article{HL2010, author = {Kohei Honda and Olivier Laurent}, title = {{An exact correspondence between a typed pi-calculus and polarised proof-nets}}, journal = {TCS}, volume = {411}, issue = {22-24}, pages = {2223--2238}, year = 2010 }

@article{HL2010, author = {Kohei Honda and Olivier Laurent}, title = {{An exact correspondence between a typed pi-calculus and polarised proof-nets}}, journal = {Theoretical Computer Science}, volume = {411}, issue = {22-24}, pages = {2223--2238}, doi = "10.1016/j.tcs.2010.01.028", year = 2010 }