Past attempts have been made to apply Girard's linear logic to Lafont's interaction nets by treating "symbois" as logical rules, however, failed to come to a signijicant explanation. In this paper, we try to model "symbols" as external axioms and use "tensor" to describe partition of auxiliary ports. We show that our solution leads to a very natural logical interpretation of the computation on interaction nets.

本文给出一个新的线性逻辑的证明网的定义并证明了所定义的证明网是线性逻辑的自然推理。和Girard的原定义相比，使用本文给出的定义来判定一个证明结构是否为证明网的时间复杂度为O（n*n），并且在证明所定义的证明网是可矢列化时更加自然和简单。

规范（specification）的目的是提供一个标准, 用以引导和评价软件系统的设计、实现和维护。本文从术语“规范”的定义出发, 讨论一个良好的软件规范必须具备的性质, 分析了形式规想半形式规范和非形式规范的优缺点, 给出了一些典型的规范系统的分类及相互间的关系。

Curry-Howard isomorphism has proved very fruitful as a methodological tool for exploiting the deep relationship among typed lambda calculus, intuitionistic logic and cartesian closed categories, A direct payoff of this has been the design of functional programming langages with powerful type systems, Limear logic is a logic of actions that seems weell suited for concurrent computation. In this paper, we establish a correspondence between Petri nets, linear logic and symmetic monoidal categories.

In 1986, J.Y. Girard discovered that usual logical implicaiton could be broken up into more clementary linear operations, Following that, he developed a new logical system, called linear logic, which appears now as a promising approach to fundamental questions arising in proof theory and in computer science, In this paper, we give a brief guide to the characteristics of linear logic, summary the recent developments and discuss the prospect of its applications to computer science.

程序设计中的并行性可以区分为逻辑并行性和物理并行性，前者是一种程序构造工具，它通过任务复合来描述程序；后者实现技术，它关心的是任务如何在处理器集合上的分配。本文将介绍一种新的并行计算模型GAMMA，其使用多重集转换技术，允许在较高的抽象层次上开发逻辑并行性，已被证明是一种有效的并行程序构造方法。

随着基于Internet 的分布式计算的兴起，如何在确保系统安全的情况下有效地使用网络上的各种计算资源已成为计算机科学的研究热点之一。由Necula 和Lee 提出的自带证明代码（PCC）概念被认为是一种可行的技术，文中研究PCC 技术所涉及的技术问题，分析比较了PCC 和其他安全技术的适应性，指出了该技术的优点和限制，提出了相应的改进措施，探讨了其在远程高性能并行计算及可移动代码迁移系统中应用的可能性。

交互作用网是Lafont[1]于1990年在POPL会议上提出的一种程序设计语言，本文我们从证明和程序的关系出发，使用线性逻辑作为一中长跑 集成逻辑讨论交互作用网的理论性质，得到下述结论：·网上的结点辅助商品的划分可表示成相应类型的张量积；·网上的计算等价于线性矢列演算中Principal-Cut的消去；·对于任何一个交互作用网，如果存在一个线性矢列演算与之对应，则该网是简单的。

使用函数式语言书写的程序包含了稳式的并行性。由于表达式可以以任意次序计值, 因此无需显式的并行结构来管理并行性, 且可以非常方便地在并行计算机体系结构上实现, 程序正确性的证明也相对简单。但一般说来在函数式语言并行实现过程中所开发的是细颗粒度的并行性, 它的管理开梢较大。本文在纯函数式语言Miranda中引入两个并行进程构造子, 它们的使用使得在粗颗粒度上管理并发进程的产生、执行、通讯、成为可能，从而提高了程序的执行效率。

所谓的逻辑式程序设计它两个逻辑层次，外部逻辑和内部逻辑，前者描述对象之间的逻辑关系，而后者涉及目标求解遵循的逻辑法则。如PROLOG,它的外部逻辑是古典逻辑，而其计算遵循的，我们将证明可以使用线性逻辑中的记法加以刻画。西方从证明论角度出发，研究PROLOG目标求解成功或失败的公理化，并说明对任一给定的程序P，可定义一个线性理论LT（P），关于该理论，PROLOG目标求解是正确且完备的。