木下 佳樹 研究室

木下佳樹研究室

理学部／情報科学科

プログラミングの原理を科学する

コンピュータプログラムとオープンシステムディペンダビリティに関する書籍

当研究室のテーマである「プログラミング科学」とは、プログラムとは何か？（算譜意味論）、正しいプログラムとは？（算譜検証論）、システムが妥当とは？（妥当性確認論）という三つの問いから出発する、プログラム構築に関する科学です。
算譜意味論には圏論、普遍代数などを用います。算譜検証論には、命題論理や述語論理だけでなく、時相論理や構成的型理論などの特別な体系を用います。妥当性確認論では、アシュランスケースと呼ばれる形式を用います。
当研究室では、算譜意味論や算譜検証論の手法を応用した形式アシュランスケース、システム利用者を含めた情報処理システムライフサイクルなどを数理科学の立場から研究しています。

Photos