Software development environment based on integration of computation and logic

基于计算与逻辑融合的软件开发环境

• 批准号: 19300007
• 负责人: SATO Masahiko
• 金额: $ 8.74万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2007
• 资助国家: 日本
• 起止时间: 2007 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19300007/
• 关键词: 自然枠組; ソフトウェア開発; ソフトウェア検証; メタ言語; 式の理論; メタ理論; 抽象操作; メタ変数

This project proposes the Natural Framework (NF) as a theoretical foundation of software development environments. NF is a logical framework in which we can describe both calculus systems and logical systems, and hence we can uniformly discuss reliability of both software and meta theories for software. In this project, in order to realize NF, (1) a formal theory of meta variables has been proposed, (2) a syntactic theory for NF has been proposed, and (3) a programming language to implement NF has been designed.

该项目提出了自然框架（NF）作为软件开发环境的理论基础。NF是一个逻辑框架，在这个框架中我们可以描述演算系统和逻辑系统，因此我们可以统一讨论软件和软件Meta理论的可靠性。为了实现NF，本文提出了Meta变量的形式化理论，提出了NF的语法理论，设计了实现NF的程序设计语言。

项目成果

A Framework for Checking Proofs Naturally

自然检查证明的框架

• 发表时间: 2008
• 期刊: Journal of Intelligent Information System 31
• 作者: Higa Y;Nguyen T. Y;Kawada H;TranH. S;Nguyen T. H;Takagi M.;佐藤雅彦
• 通讯作者: 佐藤雅彦

ホームページ等。

主页等

External and Internal Syntax of the Lambda-Calculus

Lambda 演算的外部和内部语法

• 发表时间: 2008
• 期刊: The Austrian-Japanese Workshop on Symbolic Computation in Software Science (SCSS 2008)
• 作者: Higa Y;Nguyen T.Y;Kawada H;Tran H.S;Nguyen T.H;Takagi M.;佐藤雅彦
• 通讯作者: 佐藤雅彦

フレーゲの計算機科学への影響

弗雷格对计算机科学的影响

• 发表时间: 2005
• 期刊: 科学哲学 38(2)
• 作者: 中澤 巧爾;龍田 真;佐藤 雅彦
• 通讯作者: 佐藤 雅彦

A logical foundation for environment classifiers, Proceedings of

环境分类器的逻辑基础，论文集

• 发表时间: 2009
• 期刊: the 9th International Conference on Typed Lambda-Calculi and Applications(TLCA'09) LNCS5608
• 作者: Takeshi Tsukada;Ats I arashi
• 通讯作者: Ats I arashi