MobilityReadingGroup

An exact correspondence between a typed pi-calculus and polarised proof-nets

Kohei HONDA, Olivier LAURENT

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
}