Girard's Linear Logic and its Application

建立了基于线性逻辑及其语义的各种计算模型。(1)在证明-搜索范式的框架下，我们研究了基于线性逻辑的进程演算的并发进程计算模型。我们建立了用于分析并发进程的语义技术。例如，我们对阶段语义进行了修改，得到了可观测过程的语义刻画定理。(2)在归约范式的框架下，研究了基于线性逻辑的类型化函数式程序设计语言的计算模型。我们建立了一个新的语义框架来证明强归一化性质。我们的方法是非常强大的，因为我们统一地证明了各种不同逻辑系统的强归一化能力。(3)应用上述语义方法建立了轻线性逻辑的语义，它是线性逻辑的一个特殊的子系统，具有多项式时间计算的特点。然后研究了基于该语义框架的多项式计算模型。

We established various computation models based on linear logic and their sematics. (1) In the framework of the proof-search paradigm we investigate a computation model for concurrent processes for a linear-logic based process calculus. We established semantic techniques for analysing the concurrent processes. For example, we modified the phase semantics to obtain a semantic characterization theorem for observable processes. (2) In the framework of the reduction paradigm we investigate a computation model for linear logic based typed functional programming languages. We established a new semantic framework to prove the strong normalization property. Our method is very powerful in the sense that the strong normalizability for various different logical systems are shown uniformly. (3) We applied the above semantic method to establish the semantics for Light Linear Logic, a special subsystem of Linear Logic which characterizes the polynomial-time computation. Then we investigated the polynomial computation model using this semantic framework.