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

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

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.