Application of Logic to Programming Language Theory

逻辑在编程语言理论中的应用

基本信息

批准号：
05808030
负责人：
OKADA Mitsuhiro
金额：
$ 1.22万
依托单位：
Keio University, Faculty of Letters
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1993
资助国家：
日本
起止时间：
1993 至 1994
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-05808030/
关键词：
Multi-paradigm programming Higher order term rewriting Proof theory Algebraic specification Type theory Typed lambda calculus Termination problem Mobile linear logic 項書き換えシステム高階等式言語論理的プログラム言語プログラム検証

项目摘要

We established a logical computation model for a multi-paradigm programming language which combines the two programming paradigms, that for polymorphic typed fanctional language and that for algebraic (equational) specification language. For that purpose, we combined the two logical computation models, polymorphically typed lambda calculus on one hand a higher order and first order term rewrite system on the other hand. In particular, we established a termination criterion and a confluence criterion for the combined computation model. We also implemented the resulting combined programming language.We also studied mobile linear logic, which is an extension of the usual linear logic, in order to capture the paradigm of higher order concurrent programming. Here, our mobile linear logic has the expressive power of Milner's pi-calculus (a calculus for concurrency systems with mobile message passings) and its natural extension (with higher order mobile message passings). The higher order (strong) mobile message passing mechanism was realized by the logical language with self-referential predicates. Such a logical language was introduced by restricting the use of higher order abstract terms, which avoided Russell's paradox even though some sort of self-referential predicates was permitted.

我们为多范式编程语言建立了一个逻辑计算模型，该模型结合了两个编程范式，该模型用于多态性键入的粉丝倾向语言以及代数（equabitation）规范语言。为此，我们将两个逻辑计算模型结合在一起，一方面是多态键入的lambda微积分，另一方面是高阶和一阶术语重写系统。特别是，我们为组合计算模型建立了终止标准和汇合标准。我们还实施了由此产生的组合编程语言。我们还研究了移动线性逻辑，这是通常的线性逻辑的扩展，以捕获高阶同时编程的范式。在这里，我们的移动线性逻辑具有Milner的Pi-Calculus（一种具有移动消息传递的并发系统的微积分）及其自然扩展（具有高阶移动消息传递）的表达能力。高阶（强）移动消息传递机制是通过具有自指谓词的逻辑语言实现的。通过限制使用高阶抽象术语来引入这种逻辑语言，即使允许某种自我指出的谓词，这种语言也避免了罗素的悖论。