研究分野
- 書き換えシステム
- 定理自動証明
- ソフトウェア基礎
研究内容
本研究室では，論理学と計算機科学に基づく理論的なアプローチによって，ソフトウェアやその計算を厳密に取り扱うことを目指しています． これにより，ソフトウェアの安全性や信頼性を高めるためのさまざまな手法に貢献したいと考えています． 具体的には，主に，項書き換えシステム(term rewriting systems)とよばれる等式推論に基づく計算モデルに基づいた検証理論や自動証明法についての研究を行います． 等式推論は，人間によって直観的に把握しやすい推論方法であるばかりでなく，場合によっては，リダクションによって効率的に推論を実現することが可能です． また，項書き換えシステムを対象とすることで，ソフトウェアやその性質に対する検証が，理論的な見通しの面からも，技術的な自動証明の面からも容易になると考えています． 項書き換えシステムやさまざまな書き換えシステムにおける検証理論や検証技術などの基礎研究，および，書き換えシステムを用いた定理自動証明などの応用研究を通じて，計算と証明を融合した新しいパラダイムの実現を目指します．
配属や進学を希望される学生の皆さんへの研究室紹介(スライド)
リンク
- 外山先生(東北大学名誉教授)による項書き換えシステム入門
- 浜名先生(群馬大学)によるプログラミング言語研究のための(高階)項書換え系入門
- 書き換えに関する国際スクール (ISR) (英語)
- FSCD (項書き換え分野の国際会議)