Application of type theory and linear logic for Programming Languages

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

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.