安全・安心な環境適応型ソフトウェアの基礎理論に関する研究

安全可靠环境自适应软件基础理论研究

基本信息

批准号：
18049044
负责人：
五十嵐淳
金额：
$ 2.11万
依托单位：
Kyoto University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas
财政年份：
2006
资助国家：
日本
起止时间：
2006 至无数据
项目状态：
已结题

项目摘要

本研究では,ヘテロジニアスな環境におけるソフトウェア構築を容易にする環境適応型ソフトウェアを提案し,そのようなソフトウェアの意味論と,安全性向上のための型理論などの基礎理論を研究してきた.本年度の成果は以下の通り.プログラム特化の安全性確保のための型理論構築論理の証明体系と計算体系の間の一般的な同型対応を利用して,線形時間時相論理の証明体系からプログラム特化を行う多段階計算のための型付計算体系を構築し,その型理論による体系の安全性などを証明した.また,そのような計算体系に基づく,簡単なプログラミング言語を設計するとともに,実装方式として抽象機械とその機械語へのコンパイル技法を研究し,予備的な結果を得た.明示的環境・メタ変数に関する意味論の研究実行時メタ情報を抽象化した明示的環境を取り入れた計算体系の意味論研究に取り組み,強正規化性(停止性)という計算体系の重要な性質を保つ範囲で,よりきめ細かな環境特化の制御を行うことが可能な計算体系を構築するという成果をあげた.継続に関する意味論・型理論の研究実行制御に関するメタ情報を抽象化した継続に関する意味論・型理論の研究を行い,継続を第一級の値として扱うための言語機構である階層型shift/resetを使うプログラムの安全性確保のための型システムや,停止性の一般的な証明技法を構築するなどの成果をあげた.

在这项研究中，我们提出了促进在异质环境中促进软件构建的环境自适应软件，并研究了此类软件的语义和基本理论，例如用于提高安全性的类型理论。今年的结果如下。使用类型理论构建逻辑的证明系统之间的一般同构对应，以确保程序专业化的安全性，我们为多阶段计算构建了一个键入的计算系统，该计算系统从线性时空逻辑的证明系统中专门研究，并基于该类型的理论证明了系统的安全性。此外，我们设计了一种基于这种计算系统的简单编程语言，并针对抽象机及其编译技术作为实现方法设计了汇编技术。我们研究了明确环境和Metavariables的语义。我们对计算系统的语义研究进行了研究，该计算系统结合了明确的环境，这些环境在运行时抽象了元信息，并在构建计算系统方面取得了成就，该计算系统允许在维持计算系统重要属性的范围内更详细的环境专业化，例如强大的归一化（停止能力）。关于延续的语义和类型理论的研究，并已经对有关延续的语义和类型理论进行了研究，该研究摘要有关执行控制的元信息，并实现了诸如构建类型系统的结果，以确保使用层次移动/重置的程序的安全性，一种使用层次移动/重置的程序的安全性，一种将延续作为第一阶段价值处理的语言机制以及用于停止的一般证明技术。

项目成果

期刊论文数量（6）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Proving noninterference by fully complete translation to the simply typed λ-calculus

通过完全转换为简单类型的 λ 演算来证明无干扰

DOI：
发表时间：
期刊：
Proceedings of the 11th Annual Asian Computing Science Conference (ASIAN' 06) (印刷中)
影响因子：
0
作者：
Naokata Shikuma;Atsushi Igarashi
通讯作者：
Atsushi Igarashi

Union types for object-oriented programming

面向对象编程的联合类型

DOI：
发表时间：
2007
期刊：
Journal of Object Technology 6・2
影响因子：
0
作者：
Igarashi;A.
通讯作者：
A.

A modal type system for multi-level generating extensions with persistent code

具有持久代码的多级生成扩展的模态类型系统

DOI：
发表时间：
2006
期刊：
Proceedings of the 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
影响因子：
0
作者：
Yoshihiro Yuse;Atsushi Igarashi
通讯作者：
Atsushi Igarashi

Strong normalization proofs by CPS-translations

通过 CPS 翻译进行强有力的标准化证明

DOI：
发表时间：
2006
期刊：
Information Processing Letters 99
影响因子：
0
作者：
Satoshi Ikeda;Koji Nakazawa
通讯作者：
Koji Nakazawa

計算と論理のための自然枠組NF/CAL

计算和逻辑 NF/CAL 的自然框架

DOI：
发表时间：
2006
期刊：
コンピュータソフトウェア 23・3
影响因子：
0
作者：
Satoshi Ikeda;Koji Nakazawa;佐藤雅彦
通讯作者：
佐藤雅彦

DOI：
{{ item.doi }}
发表时间：
{{ item.publish_year }}
期刊：
{{ item.journal_name }}
影响因子：
{{ item.factor }}
作者：
{{ item.authors }}
通讯作者：
{{ item.author }}

数据更新时间：{{ journalArticles.updateTime }}

作者：
{{ item.author }}

数据更新时间：{{ monograph.updateTime }}

作者：
{{ item.author }}

数据更新时间：{{ sciAawards.updateTime }}

作者：
{{ item.author }}

数据更新时间：{{ conferencePapers.updateTime }}

作者：
{{ item.author }}

数据更新时间：{{ patent.updateTime }}

五十嵐淳其他文献

An AOP Implementation Framework for Extending Join Point Models

扩展连接点模型的AOP实现框架

DOI：
发表时间：
2004
期刊：
Proceedings of ECOOP2004 Workshop on Reflection, AOP and Meta-Data for Software Evolution (RAM-SE'04)
影响因子：
0
作者：
Kouhei Sakurai;Atsushi Igarashi;Futoshi Iwama;Kouhei Sakurai;Atsushi Igarashi;Futoshi Iwama;Atsushi Igarashi;四野見秀明;古川陽;櫻井孝平;神尾貴博;Atsushi Igarashi;Tetsuo Tamai;Hideaki Shinomi;Toshihiko Tsumaki;Naoyasu Ubayashi;Yoshiyuki Mihara;Hidehiko Masuhara;四野見秀明;森山元喜;篠塚卓;黒田滋樹;中島震;大根田裕一;青谷知幸;遠藤侑介;Yudai Yamazaki;Tomoyuki Aotani;Ysuke Endoh;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;Tetsuo Tamai;Atsushi Igarashi;Yusuke Endoh;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;Atsushi Igarashi;四野見秀明;古川陽;櫻井孝平;神尾貴博;Atsushi Igarashi;Tetsuo Tamai;Hideaki Shinomi;Toshihiko Tsumaki;Naoyasu Ubayashi;Yoshiyuki Mihara;Hidehiko Masuhara;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Kamina;中島震;玉井哲雄;河内一了;五十嵐淳;Tetsuo Kamina;Naoyasu Ubayashi;Shuhei Sato;Kouhei Sakurai;Shin Nakajima;Shin Nakajima;Yoshikazu Kato;神尾貴博;中島震;鵜林尚靖;柳楽秀士;立沢秀晃;紙名哲生;櫻井孝平;櫻井孝平;櫻井孝平;Takahiro Kamio;玉井哲雄;河内一了;五十嵐淳;Naoyasu Ubayashi
通讯作者：
Naoyasu Ubayashi

文脈依存資源使用解析のための型システム

用于上下文相关资源使用分析的类型系统

DOI：
发表时间：
2008
期刊：
影响因子：
0
作者：
仲井間達也;五十嵐淳;小林直樹
通讯作者：
小林直樹

役割に基づく計算モデルEpsilonを用いたデザインパターン再利用化の促進

使用基于角色的计算模型 Epsilon 促进设计模式重用

DOI：
发表时间：
2003
期刊：
日本ソフトウェア科学会第20回大会講演論文集
影响因子：
0
作者：
Kouhei Sakurai;Atsushi Igarashi;Futoshi Iwama;Kouhei Sakurai;Atsushi Igarashi;Futoshi Iwama;Atsushi Igarashi;四野見秀明;古川陽;櫻井孝平;神尾貴博;Atsushi Igarashi;Tetsuo Tamai;Hideaki Shinomi;Toshihiko Tsumaki;Naoyasu Ubayashi;Yoshiyuki Mihara;Hidehiko Masuhara;四野見秀明;森山元喜;篠塚卓;黒田滋樹;中島震;大根田裕一;青谷知幸;遠藤侑介;Yudai Yamazaki;Tomoyuki Aotani;Ysuke Endoh;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;Tetsuo Tamai;Atsushi Igarashi;Yusuke Endoh;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;Atsushi Igarashi;四野見秀明;古川陽;櫻井孝平;神尾貴博;Atsushi Igarashi;Tetsuo Tamai;Hideaki Shinomi;Toshihiko Tsumaki;Naoyasu Ubayashi;Yoshiyuki Mihara;Hidehiko Masuhara;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Kamina;中島震;玉井哲雄;河内一了;五十嵐淳;Tetsuo Kamina;Naoyasu Ubayashi;Shuhei Sato;Kouhei Sakurai;Shin Nakajima;Shin Nakajima;Yoshikazu Kato;神尾貴博;中島震;鵜林尚靖;柳楽秀士;立沢秀晃;紙名哲生;櫻井孝平;櫻井孝平;櫻井孝平;Takahiro Kamio;玉井哲雄;河内一了;五十嵐淳;Naoyasu Ubayashi;Shuhei Sato;Shin Nakajima;Shin Nakajima;Yoshikazu Kato;紙名哲生;Tetsuo Kamina;Atsushi Igarashi;Hidehiko Masuhara;Hidehiko Masuhara;Hidehiko Masuhara;Tetsuo Kamina;Tomoyuki Kaneko;柳楽秀士;中島震;中島震;河内一了;紙名哲生;紙名哲生;佐藤匡剛
通讯作者：
佐藤匡剛

Lisp拡張によるパターンマッチを用いたXML文書処理系

使用 Lisp 扩展的模式匹配的 XML 文档处理系统

DOI：
发表时间：
2003
期刊：
オブジェクト指向2003シンポジウム
影响因子：
0
作者：
Kouhei Sakurai;Atsushi Igarashi;Futoshi Iwama;Kouhei Sakurai;Atsushi Igarashi;Futoshi Iwama;Atsushi Igarashi;四野見秀明;古川陽;櫻井孝平;神尾貴博;Atsushi Igarashi;Tetsuo Tamai;Hideaki Shinomi;Toshihiko Tsumaki;Naoyasu Ubayashi;Yoshiyuki Mihara;Hidehiko Masuhara;四野見秀明;森山元喜;篠塚卓;黒田滋樹;中島震;大根田裕一;青谷知幸;遠藤侑介;Yudai Yamazaki;Tomoyuki Aotani;Ysuke Endoh;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;Tetsuo Tamai;Atsushi Igarashi;Yusuke Endoh;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;Atsushi Igarashi;四野見秀明;古川陽;櫻井孝平;神尾貴博;Atsushi Igarashi;Tetsuo Tamai;Hideaki Shinomi;Toshihiko Tsumaki;Naoyasu Ubayashi;Yoshiyuki Mihara;Hidehiko Masuhara;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Kamina;中島震;玉井哲雄;河内一了;五十嵐淳;Tetsuo Kamina;Naoyasu Ubayashi;Shuhei Sato;Kouhei Sakurai;Shin Nakajima;Shin Nakajima;Yoshikazu Kato;神尾貴博;中島震;鵜林尚靖;柳楽秀士;立沢秀晃;紙名哲生;櫻井孝平;櫻井孝平;櫻井孝平;Takahiro Kamio;玉井哲雄;河内一了;五十嵐淳;Naoyasu Ubayashi;Shuhei Sato;Shin Nakajima;Shin Nakajima;Yoshikazu Kato;紙名哲生;Tetsuo Kamina;Atsushi Igarashi;Hidehiko Masuhara;Hidehiko Masuhara;Hidehiko Masuhara;Tetsuo Kamina;Tomoyuki Kaneko;柳楽秀士;中島震;中島震;河内一了;紙名哲生
通讯作者：
紙名哲生

ソフトウエア工学の基礎

软件工程基础

DOI：
发表时间：
2004
期刊：
影响因子：
0
作者：
Kouhei Sakurai;Atsushi Igarashi;Futoshi Iwama;Kouhei Sakurai;Atsushi Igarashi;Futoshi Iwama;Atsushi Igarashi;四野見秀明;古川陽;櫻井孝平;神尾貴博;Atsushi Igarashi;Tetsuo Tamai;Hideaki Shinomi;Toshihiko Tsumaki;Naoyasu Ubayashi;Yoshiyuki Mihara;Hidehiko Masuhara;四野見秀明;森山元喜;篠塚卓;黒田滋樹;中島震;大根田裕一;青谷知幸;遠藤侑介;Yudai Yamazaki;Tomoyuki Aotani;Ysuke Endoh;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;Tetsuo Tamai;Atsushi Igarashi;Yusuke Endoh;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;Atsushi Igarashi;四野見秀明;古川陽;櫻井孝平;神尾貴博;Atsushi Igarashi;Tetsuo Tamai;Hideaki Shinomi;Toshihiko Tsumaki;Naoyasu Ubayashi;Yoshiyuki Mihara;Hidehiko Masuhara;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Kamina;中島震;玉井哲雄;河内一了;五十嵐淳;Tetsuo Kamina;Naoyasu Ubayashi;Shuhei Sato;Kouhei Sakurai;Shin Nakajima;Shin Nakajima;Yoshikazu Kato;神尾貴博;中島震;鵜林尚靖;柳楽秀士;立沢秀晃;紙名哲生;櫻井孝平;櫻井孝平;櫻井孝平;Takahiro Kamio;玉井哲雄;河内一了;五十嵐淳;Naoyasu Ubayashi;Shuhei Sato;Shin Nakajima;Shin Nakajima;Yoshikazu Kato;紙名哲生;Tetsuo Kamina;Atsushi Igarashi;Hidehiko Masuhara;Hidehiko Masuhara;Hidehiko Masuhara;Tetsuo Kamina;Tomoyuki Kaneko;柳楽秀士;中島震;中島震;河内一了;紙名哲生;紙名哲生;佐藤匡剛;紙名哲生;金子知適;小田原大;金子知適;田中哲朗;Atsushi Igarashi;Hidehiko Masuhara;中島震;鵜林尚靖;Atsushi Igarashi;金子知適;Atsushi Igarashi;金子知適;Buntaro Shizuki;Mikio Aoyama;Atsushi Igarashi;Susumu Yamazaki;Y.Ando;Tetsuo Tamai;Tetsuo Kamina;Reynald Affeldt;Tetsuo Tamai;Tetsuo Tamai;Atsushi Igarashi;Tomoyuki Kaneko;Mikio Aoyama;Mikio Aoyama;紙名哲生;紙名哲生;青山幹雄;青山幹雄;青山幹雄;Atsushi Igarashi;Atsushi Igarashi;Buntaro Shizuki;Mikio Aoyama;Tetsuo Kamina;Atsushi Igarashi;Atsushi Igarashi;Tetsuo Tamai;玉井哲雄
通讯作者：
玉井哲雄