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

Authors :: Olivier Laurent
Kohei Honda
Department of Computer Science
Royal Holloway [University of London] (RHUL)
Preuves, Programmes et Systèmes (PPS)
Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)
ANR-07-BLAN-0324,CHOCO,Curry-Howard pour la concurrence(2007)
Source :: Theoretical Computer Science, Theoretical Computer Science, Elsevier, 2010, 411 (22--24), pp.2223--2238. ⟨10.1016/j.tcs.2010.01.028⟩
Publication Year :: 2010
Publisher :: Elsevier BV, 2010.
Abstract: International audience; 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) (for proof-nets) and Kohei Honda et al. (2004) (for the π-calculus).