权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Application of type theory and linear logic for Programming Languages

类型论和线性逻辑在编程语言中的应用

基本信息

批准号：
07044093
负责人：
OKADA Mitsuhiro
金额：
$ 6.53万
依托单位：
Keio University
依托单位国家：
日本
项目类别：
Grant-in-Aid for international Scientific Research
财政年份：
1995
资助国家：
日本
起止时间：
1995 至 1996
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07044093/
关键词：
Type Theory Linear Logic Constructive Proof Programming Languages Program Verification Program Semantics Concurrency Intuitionistic Logic Proof Theory 直観主義理論プログラム言語

项目摘要

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.

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