|
|||||
|
|
| 线性逻辑和态极逻辑引论(Ⅱ) | |
| 引用本文： | Pierre—Louis Curien. 线性逻辑和态极逻辑引论(Ⅱ)[J]. 数学进展, 2006, 35(1): 1-44 |
| 作者姓名： | Pierre—Louis Curien |
| 作者单位： | Pierre-Louis Curien（CNRS & Université Paris Ⅶ） |
| 摘 要： | 本文是《线性逻辑和态极逻辑引论》一文的第二部分。文章致力于证明网(第1节)和态极逻辑(第2,3,4和5节)证明网部分尽管局限于其积线性逻辑框架,但仍不失其重要性。线性逻辑和态极逻辑均为Girard所创建,近期所发展起来的态极逻辑旨在于进一步揭示计算和逻辑的基本交互作用的本质。我们希望本文能对这一新的理论带来一些计算机科学方面的启示。 |
| 关 键 词： | 切消 线性逻辑 计算机科学中的逻辑 计算的交互模式 语义 程序设计语言 |
| 文章编号： | 1000-0917（2006）01-0001-44 |
| 收稿时间： | 2004-04-09 |
| 修稿时间： | 2004-04-09 |
Introduction to Linear Logic and Ludics (Ⅱ) |
|
| Pierre-Louis Curien. Introduction to Linear Logic and Ludics (Ⅱ)[J]. Advances in Mathematics(China), 2006, 35(1): 1-44 | |
| Authors: | Pierre-Louis Curien |
| Affiliation: | CNRS & Université Paris Ⅶ |
| Abstract: | This paper is the second part of an introduction to linear logic and ludics, both due to Girard. It is devoted to proof nets, in the limited, yet central, framework of multiplicative linear logic (Section 1) and to ludics, which has been recently developped in an aim of further unveiling the fundamental interactive nature of computation and logic (Sections 2, 3, 4, and 5). We hope to offer a few computer science insights into this new theory. |
| Keywords: | cut-elimination linear logic logic in computer science interactive modes of computation semantics programming languages |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |