Application of type theory and linear logic for Programming Languages

类型理论利用逻辑机制为程序验证和系统程序开发提供了一个理想的形式化框架。另一方面，线性逻辑提供了表示计算资源和并发计算的框架。因此，将这两种理论结合起来，设计一种功能强大的新型程序设计语言及其程序开发工具，似乎是非常有前途的。为此，我们研究了线性类型语言这一组合形式框架的理论基础，特别是为线性类型语言建立了许多重要的语义学理论。例如，将阶段语义扩展到动态阶段语义，在动态阶段语义中可以进行割消和归一化证明。阶段语义也被扩展到更高阶线性类型语言。吉拉德介绍了轻线性逻辑，它被认为是线性逻辑的一个重要系统，因为它以一种纯逻辑的方式表征了多项式时间计算。我们将我们的阶段语义学理论应用于轻线性逻辑，建立了轻线性逻辑中重要概念的阶段语义刻画。连贯的语义也有了很大的改进。例如，连贯性Banach空间语义是线性类型语言的一种很有前途的指称语义，它是在法国团队负责人J-Y.Girard访问我们的团队在日本时开发的。在我们的项目研究中，已经针对线性类型语言提出了各种重要的计算模型。特别是，从编程范式的角度研究了归约范式和证据搜索范式，从编程语言的角度研究了证据搜索范式。

Type THeory is provides an ideal formal framework for program verification and systematic program development utililzing the logical mechanism. On the other hand, linear logic provides the framework for expressing computational resources and concurrent computation. Therefore, it seems very promising to combine these two theories in order to design a powerful and new programming language and its program development tools. For this purpose, we have investigated the theoretical foundations for this combined formal framework, linear type language.In particular, we established verious important semantics theories for the linear type language. For example, phase semantics is extended to a dynamic phase semantics in which cut-elimination and normalization proofs can be performed. Phase semantics is also extended to higher order linear type languages. Girard introduced Light Linear Logic, which is considered an impotant sybsystem of linear logic since it characterized the polynomial time computation in a purely logical way. We applied our phase semantics theory to Light Linear Logic and established phase semantic characterization of the important concepts used in Light Linear Logic. The coherence semantics has also been very much improved. For example, Coherence Banach Space Semantics, which is a promising denotational semantics for the linear type language, was developped when the French team leader, J-Y.Girard, visited our group in Japan. Various important computation models for the linear type language have been proposed in our project research. In particular, the reduction paradigm and the proof-search paradigm were studied from the programming paradigm and the proof- search paradigm were studied from the programming languages point of view.