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

被引：22

作者：

Honda, Kohei ^{[2
]}

Laurent, Olivier ^{[1
]}

机构：

[1] Univ Paris 07, CNRS, Preuves Programmes Syst, F-75221 Paris 05, France

[2] Univ London, Dept Comp Sci, London WC1E 7HU, England

来源：

THEORETICAL COMPUTER SCIENCE | 2010年 / 411卷 / 22-24期

关键词：

Pi-calculus; Proof-nets; Processes; Logics; Proofs; Types; Interaction; Concurrency; Linear Logic; Polarity; Embedding; Determinism; Non-determinism; EQUIVALENCE;

D O I：

10.1016/j.tcs.2010.01.028

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents an exact correspondence in typing and dynamics between polarised linear logic and a typed pi-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 pi-calculus). (C) 2010 Elsevier B.V. All rights reserved.

引用

页码：2223 / 2238

页数：16

共 42 条

[1] Abramsky S, 2000, INFORM COMPUT, V163, P409, DOI [10.1006/inco.2000.2930, 10.1006/inco2000.2930]
[2] PROOFS AS PROCESSES
ABRAMSKY, S
[J]. THEORETICAL COMPUTER SCIENCE, 1994, 135 (01) : 5 - 9
[3] Agha G.Actors., 1986, MODEL CONCURRENT COM
[4] Baeten J.C.M., 1990, Process Algebra
[5] BEFFARA E, 2005, THEORETICAL COMPUTER, V356
[6] A Concurrent Model for Linear Logic
Beffara, Emmanuel
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 155 : 147 - 168
[7] ON THE PI-CALCULUS AND LINEAR LOGIC
BELLIN, G
SCOTT, PJ
[J]. THEORETICAL COMPUTER SCIENCE, 1994, 135 (01) : 11 - 65
[8] Berger M, 2001, LECT NOTES COMPUT SC, V2044, P29
[9] BERGER M, 2003, LECT NOTES COMPUTER, V2620
[10] Boudol G, 1992, Rapport de Recherche 1702

← 1 2 3 4 5 →