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

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 [Lau03] (for proof-nets) and [HYB04] (for the -calculus).

• Type: Journal
• Year: 2010
• Where: TCS
• Authors: Kohei Honda, Olivier Laurent
• Keywords: Exact Correspondence, Respective Formalisms, Respective Incremental Constraints, TCS 2010, Theoretical Computer Science