Application of Logic to Programming Language Theory

点击翻译按钮获取中文摘要

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.