Interaction nets
Interaction nets
复制标题
互动网
DOI：
--
复制
发表时间：
1989
期刊：
影响因子：
--
通讯作者：
Yves Lafont
中科院分区：
文献类型：
--
作者：
Yves Lafont
我们提出了一种新的编程语言，具有以下特点：
<list><item>一个简单的图重写语义，
</item><item>构造函数和析构函数之间完全对称，
</item><item>确定性和无死锁（微观）并行的类型规程。
</item></list><italic>交互网</italic>推广了吉拉德的线性逻辑<italic>证明网</italic>，并说明了<italic>集成逻辑</italic>方法的优势，而不是<italic>外部</italic>的。换句话说，我们并没有试图设计一种描述某个给定计算系统行为的逻辑，而是设计一种类型规则已经（几乎）是逻辑的编程语言。
事实上，我们几乎不会提到逻辑，因为我们采用了一种天真和实用主义的风格。这种语言的一个典型应用是设计交互式软件，如编辑器或窗口管理器。
We propose a new kind of programming language, with the following features:
<list><item>a simple graph rewriting semantics,
</item><item>a complete symmetry between constructors and destructors,
</item><item>a type discipline for deterministic and deadlock-free (microscopic) parallelism.
</item></list><italic>Interaction nets</italic> generalize Girard's <italic>proof nets</italic> of linear logic and illustrate the advantage of an <italic>integrated logic</italic> approach, as opposed to the <italic>external</italic> one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.
In fact, we shall scarcely refer to logic, because we adopt a naïve and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.