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.

我们的研究目的是逻辑，特别是证明理论的应用程序，用于编程语言理论。我们特别关注线性逻辑，高阶术语重写和类型理论。在这个研究项目中，我们从语义和句法观点赋予了证据正态化（和切除）证明的一般框架。然后，我们应用了证明标准定理，为各种新的编程语言和正式规范语言提供计算模型。我们的新的证明规范化（和切除式）定理为各种逻辑编程语言提供了逻辑计算模型，包括强大的功能编程语言，可执行的代数（方程式）规范语言，逻辑编程语言，一些并发的计算语言及其组合。特别是，我们给出了一个逻辑计算模型，该模型具有诱导类型的类型推断和高阶重写的组合语言，这导致了一种新的多范式编程语言，并带有类型功能性编程语言的范式和代数规格语言的范式。我们还提供了基于证明的验证系统的计算模型，包括并发过程规范语言的验证系统以及实时多代理系统规范语言。

项目成果

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 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.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: "Theories of Types and Proofs,second edition,Memoir of Mathematical Society of Japan vol.2"Mathematical Society of Japan. (1999)

M.Okada：“类型和证明的理论，第二版，日本数学会回忆录第2卷”日本数学会。