中野 浩(なかの ひろし)

中野 浩

准教授|博士(理学)|京都大・院・理

専門分野
構成的プログラミング、型理論、λ計算
研究課題(長期)
プログラミングに現れる論理構造の解析
研究課題(短期)
オブジェクト指向プログラミングの論理

研究テーマ:プログラミングの論理

プログラミングの世界には、オブジェクトとそのクラス、継承、状態遷移、再帰、並行処理、同期、資源とその共有、排他制御、例外処理、種々のデザインパターンなど、様々な特徴的な概念・手法が現れ、ソフトウェア開発の現場では、これらを各プログラマの共通理解とすることがプロジェクトの遂行に必須となっています。 ところが、これらの概念・手法は、それぞれ個別にはかなり明快に説明することができても、その間の相互作用を含めて、これらすべてを記述・説明できるような共通の言語が存在していません。私たちは、プログラミングを人間の論理的な活動と捉え、現実のプログラマが駆使している概念や手法を分析して、その諸相を論理体系として形式化することで、その共通の言語となるものを構築することを目標としています。 最近の研究では、オブジェクト指向プログラミングに必須となる負の自己参照を許すような様相付き型付けシステム(一種の様相論理体系)を提案しています。

負の自己参照を許す型付けシステム

負の自己参照を許す型付けシステム

収束定理

収束定理

このページのトップへ戻る