発展的ソフトウェアの理論に関する研究

1999 年度 実績報告書

• 研究課題/領域番号: 09245102
• 研究機関: 東北大学
• 研究代表者: 伊藤 貴康 東北大学, 大学院・情報科学研究科, 教授 (80124551)
• 研究分担者: 米崎 直樹 東京工業大学, 大学院情報理工学研究科, 教授 (00126286) ; 坂部 俊樹 名古屋大学, 大学院工学研究科, 教授 (60111829) ; 井田 哲雄 筑波大学, 電子情報工学系, 教授 (70100047) ; 外山 芳人 北陸先端科学技術大学院大学, 教授 (00251968) ; 萩谷 昌己 東京大学, 大学院理学研究科, 教授 (30156252)
• キーワード: 発展的ソフトウェア / 発展的プログラミング機構 / ソフトウェア仕様記述 / 論理・関数型プログラミング / 書換え型メタ計算モデル / 実時間論理 / 検証系 / 検証情報

研究概要

発展的ソフトウェアの理論に関して、平成9年度および平成10年度の研究成果を踏まえて研究を行ない、次のような研究成果を得た。
1.発展的プログラミング機構の研究(担当:伊藤貴康):並列Schemeプログラミングのための健全並列化メカニズムを理論および実際のシステムを基に確立し、逐次プログラムを発展適応的に並列化するための基礎を確立した.また、発展的モジュラープログラミングの実現のため簡潔なパッケージ機能をISLISPに導入した.
2.ソフトウェア仕様作製プロセス理論の研究(担当:井田哲雄):実行可能仕様記述の基礎となる制約:関数型プログラムの計算ソフトとアルゴリズムについて基礎的な成果を得、処理系を作成した。
3.書換え型計算に基づく発展的ソフトウェアの基礎研究(担当:坂部俊樹):メタ項書換え計算モデルの諸性質とその解析手法を与えた.
4.実時間環境のための発展的ソフトウェアの理論の研究(担当:米崎直樹):時相論理および線形論理による実時間ソフトウェアの検証法と合成法を与えた.
5.検証系の検証と検証情報の発展の研究(担当:萩谷昌己):高階論理の基づく証明支援システムを用い、アルゴリズムやJAVAバイトコードのモデル検証法による検証を行う方法を与えた.
7.様相線形論理に基づく分散計算モデルおよび型システムの研究(担当:小林直樹):場所や時間を表す様相を導入した線形論理に基づく分散計算モデル、およびデッドロックフリーダムを保証する型システムについて優れた成果を得た.
8.環境の理論によるプログラミング言語の発展機構の研究(担当:西崎真也):多相環境計算体系を与え、その健全性、停止性、主要型定理を与えた.
9.書き換えシステムに基づく発展的プログラミングの研究(担当:外山芳人):書き換えシステムの分解・合成による合流性と停止性の解析法、型情報を利用した高階項書き換え系の性質の解析法などを与えた.
10.古典線形論理に基づいた論理型言語の研究(担当:田村直之):古典線形論理に基づく論理型言語を設計し、そのコンパイラを作成し、各種の拡張を行った.
11.並行システムの実行時プログラム変換の形式化の研究(担当:村上昌己):線形論理を用いた並行計算のプログラムモデルを与え、実行時の動的プログラム変換の形式化を与えた.
12.構成的論理型言語と代数的仕様言語を融合した発展的ソフトウェア開発(担当:岡田光弘):線形論理を応用した実時間並行システム仕様記述と検証、および、線形論理の拡張に関する研究を行った.

研究成果

• [文献書誌] Takayasu Ito: "A Sound Parallelization Framework for Parallel Scheme Programming, Parallel and Distributed Computing for Symbolic and Irregular Applications"World Scientific. 2-39 (2000)
• [文献書誌] 泉 信人、伊藤 貴康: "ISLISP処理系TISLのためのパッケージシステム"情報処理学会論文誌. Vol.40, No.10. 17-25 (1999)
• [文献書誌] 大崎 人士、Aart Middeldorp、井田 哲雄: "等式付き書換え系における多ソート不変性"コンピュータソフトウェア. Vol6. No.1. 33-45 (1999)
• [文献書誌] M.Marin, T.Ida, T.Suzuki: "On Reducting the Search Space of Higher-Order Lazy Narrowing"FLOPS'99 LNCS. 1722. 225-240 (1999)
• [文献書誌] 大久保 弘宗、坂部 俊樹、稲垣 康善: "オブジェクト指向プログラムに対するMessage Not Understoodフォールト検知のための型検査アルゴリズム"コンピュータソフトウェア. [掲載予定]. (2000)
• [文献書誌] 吉浦 紀晃、米崎 直樹: "適切さの論理RとERの証明力の比較"人工知能学会誌. Vol.14, No.6. 156-167 (1999)
• [文献書誌] 吉浦 紀晃、米崎 直樹: "適切さの論理ERの決定可能性"人工知能学会誌. Vol.14, No.5. 819-827 (1999)
• [文献書誌] 戸田 洋三、萩谷 昌巳: "タクティクからのプログラム抽出とその応用"情報処理学会論文誌プログラミング. Vol.40, No.SIG4. 21-32 (1999)
• [文献書誌] Koichi Takashi, Masami Hagiya: "Proving as Editing HOL Tactics"Formal Aspects of Computing. Vol.11, No.3. 343-357 (1999)
• [文献書誌] K.Satoh: "Consistency Management by Prioritized Minimal Revision"Proceedings of the International Workshop on the Principles of Software Evolution. IWPSE99. 125-129 (1999)
• [文献書誌] N.Kobayashi, B.C.Pierce, D.N.Turner: "Linearity and the Pi-Calculus"ACM Transactions on Programming Languages and Systems. [掲載予定]. (2000)
• [文献書誌] N.Kobayashi: "Quasi-Linear Types"Proc. ACM. POPL'99. 29-42 (1999)
• [文献書誌] Shin-ya Nishizakki: "Polymorphic Environment Calculus and Its Type Infernce Algorithm"Higher-Order and Symbolic Computation. [掲載予定]. (2000)
• [文献書誌] K.Kusakari, M.Nakamura, Y.Toyama: "Argument filtering transformation"Lecture Notes in Comput.. 1702. 47-61 (1999)
• [文献書誌] T.Nagaya, Y.Toyama: "Decidability for left-linear growing term rewrithing systems"Lecture Notes in Comput.. 1631. 256-270 (1999)
• [文献書誌] 番原 睦、田村 直之: "線形論理型言語のJAVA言語による処理系の設計と実装"情報処理学会論文誌プログラミング. Vol.40, No.SIG10. 1-16 (1999)
• [文献書誌] 村上 昌巳: "線形論理を用いた逐次型プロセス並列実行"情報処理学会論文誌プログラミング. Vol.40, No.SIG4. 11-20 (1999)
• [文献書誌] M.Okada: "Phase Semantic Higher Order Cut-Elimination and Normalization Proofs of Classical Linear Logic"Theoretical Computer Science. 227. 333-396 (1999)
• [文献書誌] M.Okada, K.Terui: "The Finite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-802 (1999)