Programming Language Theory Based on Logical Methods

基于逻辑方法的编程语言理论

• 批准号: 09480058
• 负责人: OKADA Mitsuhiro
• 金额: $ 1.47万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 1997
• 资助国家: 日本
• 起止时间: 1997 至 1999
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-09480058/
• 关键词: Type Theory; Linear Logic; Term Rewriting Theory; Programming Language; Proof Theory; Formal Specification and Verification; Higher Order Rewriting; Real Time System; 線形論理; プログラミング言語; 並行計算; 正規化定理; 相意味論; 証明の正規化定理; (強)停止性; 計算モデル; 高階論理; カット消

Our purpose of the research was applications of logic, in particular proof-theory, to programming language theory. We especially gave a special attention on linear logic, higher-order term rewriting and type theory. In this research project, we gave a general framework of proof-normalization (and cut-elimination) proofs from the both semantical and syntactical points of view. Then we applied our proof-normalization theorems to give computation models for various new programming languages and formal specification languages. Our new proof-normalization (and cut-elimination) theorems provide(s) logical computation models for various logical programming languages, including strongly-typed functional programming languages, executable algebraic (equational) specification languages, logic programming languages, some of concurrent process calculus languages, and their combinations. In particular, we gave a logical computation model for a combined language of typed lambda calculus with inductive type inferences and with higher order rewritings, which resulted in a new multi-paradigm programming language with both the paradigm of typed functional programming language and the paradigm of algebraic specification language. 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.

我们的研究目的是应用逻辑，特别是证明理论，编程语言理论。我们特别关注线性逻辑，高阶项重写和类型论。在这个研究项目中，我们从语义和语法的角度给出了一个一般的证明-规范化（和割-消除）证明的框架。然后，我们应用我们的证明规范化定理，给各种新的编程语言和正式规格说明语言的计算模型。我们新的证明-规范化（和割消）定理为各种逻辑编程语言提供了逻辑计算模型，包括强类型函数编程语言、可执行代数（等式）规范语言、逻辑编程语言、一些并发过程演算语言以及它们的组合。特别地，我们给出了一个逻辑计算模型的组合语言的类型lambda演算与归纳类型推理和高阶重写，这导致了一个新的多范式编程语言的范式的类型函数式编程语言和范式的代数规格说明语言。我们还给出了基于证明搜索的验证系统的计算模型，包括并发过程规范语言和实时多Agent系统规范语言的验证系统。

项目成果

M.Hamano, M. Okada: "A Relationship Among Gentzen'S Proof Reduction, Kirby-Paris Hydra Game and Buchholz's Hydra Game"Mathematical Logic quarterly. 43. 103-120 (1997)

M.Hamano、M. Okada：“Gentzen 证明还原、Kirby-Paris Hydra Game 和 Buchholzs Hydra Game 之间的关系”数理逻辑季刊。

M. Nagayama, M. Okada,: "A New Correctness Criterion for the Proof-Nets of Non Commutative Multiplicative Logic"Journal of Symbolic Logic,. to appear. (2000)

M. Nagayama，M. Okada，“非交换乘法逻辑证明网的新正确性标准”符号逻辑杂志，。

M. Takahashi, M .Okada, M. Dezani: "Special Issue on Theories of Types and Proofs"Theoretical Computer Science. to appear. (2000)

M. Takahashi、M.Okada、M. Dezani：“类型和证明理论特刊”理论计算机科学。

M.Hamano-M.Okada: "A Direct Independence Proof of Buhholz's Hydra Game" Archiev for Mathematical Logic. (to appear). (1998)

M.Hamano-M.Okada：《布霍尔茨九头蛇博弈的直接独立性证明》Archiev，数学逻辑。

M. Okada and P.J.Scott: "A Note on Rewriting Theory for Uniquiness of Iteration"Journal of Theory and Application of Categories. 6. 47-64 (1999)

M. Okada 和 P.J.Scott：“关于迭代唯一性重写理论的注释”范畴理论与应用杂志。