Applications of Type Theory and Linear Logic to Programming Language Theory

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

• 批准号: 10044094
• 负责人: OKADA Mitsuhiro
• 金额: $ 6.08万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (A).
• 财政年份: 1998
• 资助国家: 日本
• 起止时间: 1998 至 1999
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10044094/
• 关键词: Type Theory; Linear Logic; Functional Language; Programming Language; Proof Theroy; Formal specification; Formal Verification; Real Time System; プログラミング言語; プログラム意味論; 形式的プログラム検証; 形式的仕様; 情報科学の論理

Our purpose of the research was applications of type theory, intuitionistic logic and linear logic to programming language theory. We first gave various fundamental researches of semantics and the proof-normalization and proof-search techniques for type theory (equivalently, intuitionistic logic, under the Curry-Howard correspondence) and linear logic, which provided computation models of our new programming and specification/verification languages. In particular, we gave a logical computation model for a combined language of type theory with linear logic, which resulted in a new multi-paradigm programming language with both the paradigm of typed functional programming language and the paradigm of concurrent process calculus. We also gave computation models for proof-search based-verification systems, including verification systems for concurrent process specification languages and for real-time multi-agent system specification languages. In particular, we gave PSPACE-decidability result for verifications of safety and other important properties of real-time finite state system specifications based on our linear logic-based formal specification language.

我们的研究目的是将类型论、直觉逻辑和线性逻辑应用于程序设计语言理论。我们首先对语义学、类型论（相当于Curry-Howard对应下的直觉逻辑）和线性逻辑的证明规范化和证明搜索技术进行了各种基础研究，为我们的新编程语言和规范/验证语言提供了计算模型。特别地，我们给出了一种类型论与线性逻辑相结合的语言的逻辑计算模型，从而形成了一种集类型化函数式编程语言范式和并行过程演算范式于一体的新型多范式编程语言。我们还给出了基于证明搜索的验证系统的计算模型，包括并发过程规范语言的验证系统和实时多代理系统规范语言的验证系统。特别地，我们给出了基于线性逻辑的形式规范语言的PSPACE-decidability结果，用于验证实时有限状态系统规范的安全性和其他重要属性。

项目成果

M.Okada-M.Kanovitch-A.Scedrov: "Specifying Real-Time Finite State Systems by Linear Logic" Electronic Notes of Theoretical Computer Science. 16. 1-14 (1988)

M.Okada-M.Kanovitch-A.Scedrov：“通过线性逻辑指定实时有限状态系统”理论计算机科学电子笔记。

M.Okada-K.Terui: "The Finite Model Property for Various Fragments of Infuiticnistic Linear Logic" Journal of Symbolic Logic. (近刊). (1999)

M.Okada-K.Terui：“Infuiticnistic 线性逻辑各种片段的有限模型属性”符号逻辑杂志（即将出版）（1999 年）。

M. Konovitch, M. Okada and A. Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).

M. Konovitch、M. Okada 和 A. Scedrov：“轻线性逻辑的相位语义”理论计算机科学（即将出版）。

S.Hayashi: "Animating Proof systems" Theoretical Computer Science. (近刊). (1999)

S.Hayashi：“动画证明系统”理论计算机科学（即将出版）。

F. Blanqui, J-P. Jouannaud and M. Okada: "Calculus of Inductive Construction"Proc of Rewriting Technique and Application (RTA99). Springer-Lecture Note in Computer Science. 1631. 301-316 (1999)

F.布朗基，J-P。