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 [J].