Application of Logic to Programming Language Theory

我们建立了一种多范例程序设计语言的逻辑计算模型，该语言结合了多态类型函数语言和代数(等式)规格说明语言的两种程序设计范例。为此，我们结合了两种逻辑计算模型，多态类型的Lambda演算一方面是高阶项重写系统，另一方面是一阶项重写系统。特别地，我们建立了组合计算模型的终止准则和汇流准则。我们还研究了移动线性逻辑，它是通常的线性逻辑的扩展，以捕捉高阶并发程序设计的范例。在这里，我们的移动线性逻辑具有Milner的pi演算的表达能力(一种针对具有移动消息传递的并发系统的演算)及其自然扩展(具有更高阶的移动消息传递)。高阶(强)移动消息传递机制由带有自指谓词的逻辑语言实现。这种逻辑语言是通过限制高阶抽象术语的使用而引入的，这避免了罗素悖论，即使允许某种类型的自指谓词。

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.