2005 Fiscal Year Annual Research Report
充実期を迎えた線形論理の進化とその応用に関する研究
| Project/Area Number |
15300008
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
照井 一成 国立情報学研究所, 助手 (70353422)
田村 直之 神戸大学, 学術情報基盤センター, 教授 (60207248)
|
|---|
| Keywords | 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論 |
|---|
| Research Abstract |
次の3点を中心に研究を進めた。
1.昨年に引き続きReduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の確立に向けた研究を進めた。ゲーム論的意味論等の観点からの分析も加えた。(岡田・Girard等フランスグループとの共同研究)これまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にするLudics等の新たな論理体系理論の分析をGirardグループらと共同で行なった。
2.証明論と意味論の統合的見方について研究を進めた。カット消去定理等の証明論の基本定理の成立条件がPhase semanticsによる意味論的分析により明らかになることを示した。又、Simple logic等の線形論理の基礎理論に対して、証明論と意味論の統合を進めた。
3.線形論理の種々の考え方や計算モデルをタイプ理論及びプログラミング言語理論に応用した。linear-typeやquasi-linear typeを用いた静的メモリ管理の理論などについて検討した。
4.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を宗した。この目的でフランス及び米国共同研究グループとの共同研究を行なった。
|
