Design and system development of a programming language based on a temporal linear logic

在这个研究项目中，完成了以下工作：直觉时态线性逻辑系统ITLL的设计，基于ITLL的逻辑程序设计语言TLLP的设计，以及TLLP编译系统的开发。除了线性逻辑运算符，它还具有以下逻辑运算符：用于指定下一次只能使用一次的资源的模运算符0，用于指定在任何时候只能使用一次的资源的模运算符，以及用于指定在任何时候只能使用一次的资源的模运算符！它用于指定可在任何时间、任意次数使用的资源。直觉逻辑、直觉线性逻辑和直觉时态逻辑都可以嵌入到逻辑程序设计语言中。逻辑程序设计语言TLLP就是基于这种逻辑程序设计语言的，它是PROLOG和线性逻辑程序设计语言LLP的超集。在TLLP中，可以表示与时间相关的资源消耗的概念。通过扩展Miller的统一证明、Hodas的IO模型和LLP的分级IO模型的思想，给出了TLLP的计算模型。TLLP的编译器基于扩展的分级IO模型，使得TLLP程序能够有效地执行研究了线性逻辑程序设计语言到Java的翻译系统和经典线性逻辑程序设计语言的静态分析方法。

In this research project, the followings are accomplished : the design of Intuitionistic Temporal Linear Logic system ITLL, the design of a logic programming language TLLP which is based on ITLL, and the development of the compiler system of TLLP.In addition to linear logic operators, ITLL has the following logical operators : a modal operator ○ which is used to specify a resource usable only once at the next time, a modal operator □ which is used to specify a resource usable only once at any time, and a modal operator ! which is used to specify a resource usable any number of times and at any time. All of intuitionistic logic, intuitionistic linear logic, and intuitionistic temporal logic can be embedded into ITLL.Logic programming language TLLP is based on this ITLL, and it is a super-set of Prolog and a linear logic programming language LLP.In TLLP, it is possible to represent a concept of time-dependent resource consumption.Computation model of TLLP is given by extending the idea of Miller's uniform proof, Hodas's IO-model, and leveled IO-model of LLP.Compiler of TLLP is based on the extended leveled IO-model which enables the efficient execution of TLLP programs.In order to investigate a further efficient implementation of TLLP, we also studied about a translator system of a linear logic programming language into Java and about a static analysis method of a classical linear logic programming language.