研究課題
基盤研究(B)
次の3点を中心に研究を進めた。1.証明論と意味論の統合的見方について研究を進めた。カット消去定理等の証明論の基本定理の成立条件がPhase semanticsによる意味論的分析により明らかになることを示した。又、Simple logic等の線形論理の基礎理論に対して、証明論と意味論の統合を進めた。さらに、直観主義論理Phase semanticsと古典論理Phase semanticsとの密接な関係を明らかにした。Phase semanticsの成果に基づいてカット消去定理の意味論的条件の研究を進めた。2.Reduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の確立に向けた研究を進めた。ゲーム論的意味論等の観点からの分析も加えた。(岡田・Girard等フランスグループとの共同研究)これまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にするLudics等の新たな論理体系理論の分析をGirardグループらと共同で行なった。3.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を示した。この目的でフランス及び米国共同研究グループとの共同研究を行なうとともに、計3回の成果報告会を日仏共同で行った。
すべて 2006 2005 2004 2003 その他
すべて 雑誌論文 (16件) 図書 (1件)
Mathematical Structure in Computer Science (to appear)
6thlnternational Workshop on Rule-Based Programming (RULE'05) vol.147(1)
ページ: 73-92
6th International Workshop on Rule-Based Programming (RULE'05), Electronic Notes in Theoretical Computer Science (Elsevier) vol.147(1)
Workshop 0n New Approaches to Software Construction(WNASC 2004)
ページ: 45-57
Workshop on Foundations 0f Computer Security (FCS'04)
ページ: 97-113
Proceedings of the International Symposium on Software Security 2002(ISSS2003) vol.3233
ページ: 65-86
Proceedings of Foundations of Computer Security '04(affiliated with LICS'04 and ICALP'04)
La revue internationale de philosophie No.230
ページ: 449-481
Workshop on New Approaches to Software Construction (WNASC2004), Tokyo
Workshop on Foundations of Computer Security (FCS'04), Turku, Finland
Proceedings of the International Symposium on Software Security 2003 (ISSS2003), Lecture Notes in Computer Science (Springer-Verlag) vol.3233
Proceedings of Foundations of Computer Security '04 (Affiliated with LICS'04 and ICALPO4) Turku, Finland
La revue Internationale de philosophie "Intuitionism" No.230, special issue
日本ソフトウエア科学会第20回全国大会予稿集
ページ: 5 pages
20th Annual Conference of Japan Society for Software Science and Technology
ページ: 5
Mathematical Structure in Computer Science (to appear in 2006)
