研究課題
次の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.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を宗した。この目的でフランス及び米国共同研究グループとの共同研究を行なった。
すべて 2006 2005
すべて 雑誌論文 (6件) 図書 (1件)
Mathematical Structure in Computer Science 近刊
Algebra, Meaning, and Computation. A Festschrift in Honor of Prof. Joseph Goguen 近刊
Reasoning and Cognition, (Keio University Press) 近刊
Studia Logica Vol.82
ページ: 95-119
Electronic Notes in Computer Science, Invited Paper of the 6th International Workshop on Rule-Based Programming (RULE'05) vol.147(1)
ページ: 73-92
