New development of research on bug-free software construction environment

无缺陷软件构建环境研究新进展

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

We started our research by setting the goal of realizing acomputer environment for developing bug-free softwares, so that we can guarantee thesafety of computer software. We have achieved the goal by implementing a prototypesystem. In particular, as a part of the system, we implemented a programming languagewhich can be used to reason about the properties of the system itself. The interfacebetween the user and the system is also implemented by this programming language.

我们的研究目标是实现一个开发无缺陷软件的计算机环境，从而保证计算机软件的安全。我们通过实施原型系统实现了目标。特别是，作为系统的一部分，我们实现了一种编程语言，可以用来推理系统本身的属性。用户与系统之间的接口也是由该编程语言实现的。

项目成果

Viewing lambda-termsthrough maps

通过地图查看 lambda 项

• 发表时间: 2013
• 作者: Takeshi Tsukada;Atsushi Igarashi;Shunichi Yamashita;阿部修司;原田一宏;サエンコ ウラジミール;佐藤 雅彦
• 通讯作者: 佐藤 雅彦

External and internal syntax of the λ-calculus

λ 演算的外部和内部语法

• 发表时间: 2010
• 期刊: Journal of Symbolic Computation
• 影响因子: 0.7
• 作者: Masahiko Sato;Randy Pollack
• 通讯作者: Randy Pollack

A Canonical Local Representation of Binding

绑定的规范局部表示

• DOI: 10.1007/s10817-011-9229-y
• 发表时间: 2012
• 期刊: Journal of Automated Raesoning
• 作者: 藤浦祥雅;大久保弘崇;粕谷英人;山本晋一郎;Randy Pollack
• 通讯作者: Randy Pollack

Type checking and typability in domain-free lambda calculi

无域 lambda 演算中的类型检查和可打字性

• DOI: 10.1016/j.tcs.2011.06.020
• 发表时间: 2011
• 期刊: Theoretical Computer Science
• 影响因子: 1.1
• 作者: K.Nakazawa;M.Tatsuta;Y.Kameyama;H.Nakano
• 通讯作者: H.Nakano

Essence of de BruijnIndex

de BruijnIndex 的本质

• 发表时间: 2012
• 作者: 小川順平;粕谷英人;大久保弘崇;山本晋一郎;佐 藤 雅 彦
• 通讯作者: 佐 藤 雅 彦