ON THE PI-CALCULUS AND LINEAR LOGIC

被引：81

作者：

BELLIN, G ^{[1
]}

SCOTT, PJ ^{[1
]}

机构：

[1] UNIV OTTAWA,DEPT MATH,OTTAWA,ON K1N 6N5,CANADA

来源：

THEORETICAL COMPUTER SCIENCE | 1994年 / 135卷 / 01期

基金：

加拿大自然科学与工程研究理事会;

关键词：

Abstract level - Classic linear logic - Completeness - Proof structures - Soundness;

D O I：

10.1016/0304-3975(94)00104-9

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We detail Abramsky's ''proofs-as-processes'' paradigm for interpreting classical linear logic (CLL) (Girard, 1987) into a ''synchronous'' version of the pi-calculus recently proposed by Milner (1992, 1993). The translation is given at the abstract level of proof structures. We give a detailed treatment of information flow in proof-nets and show how to mirror various evaluation strategies for proof normalization. We also give soundness and completeness results for the process-calculus translations of various fragments of CLL. The paper also gives a self-contained introduction to some of the deeper proof-theory of CLL, and its process interpretation.

引用

页码：11 / 65

页数：55

共 32 条

[1] COMPUTATIONAL INTERPRETATIONS OF LINEAR LOGIC
ABRAMSKY, S
[J]. THEORETICAL COMPUTER SCIENCE, 1993, 111 (1-2) : 3 - 57
[2] NEW FOUNDATIONS FOR THE GEOMETRY OF INTERACTION
ABRAMSKY, S
JAGADEESAN, R
[J]. INFORMATION AND COMPUTATION, 1994, 111 (01) : 53 - 119
[3] GAMES AND FULL COMPLETENESS FOR MULTIPLICATIVE LINEAR LOGIC
ABRAMSKY, S
JAGADEESAN, R
[J]. JOURNAL OF SYMBOLIC LOGIC, 1994, 59 (02) : 543 - 574
[4] ABRAMSKY S, 1992, PROOFS AS PROCESSES
[5] ASPERTI A, UNPUB CAUSAL DEPENDE
[6] BELLIN G, 1990, THESIS STANFORD U
[7] BELLIN G, UNPUB PROOF NETS TYP
[8] BELLIN G, 1991, LFCS91161 U ED DEP C
[9] A GAME SEMANTICS FOR LINEAR LOGIC
BLASS, A
[J]. ANNALS OF PURE AND APPLIED LOGIC, 1992, 56 (1-3) : 183 - 220
[10] LINEAR LOGIC, COHERENCE AND DINATURALITY
BLUTE, R
[J]. THEORETICAL COMPUTER SCIENCE, 1993, 115 (01) : 3 - 41

← 1 2 3 4 →