木下 佳樹 研究室

理学部／情報科学科

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

木下 佳樹 研究室

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

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

Photos

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

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

Kinoshita Yoshiki

木下　佳樹 教授

[理学部／情報科学科]

専門分野
  • ソフトウェア科学
  • プログラム意味論
関連リンク

PROFESSOR's VOICE

意図通りに動くプログラム構築を研究

プログラム「で」研究するのではなく、プログラム「を」研究します。プログラムが意図通りに動くことを確信できるようにするために、プログラムや関連文書を解析する方法を、数理科学の立場から研究します。

木下　佳樹教授

SHARE

一覧に戻る

Recommend

この研究室もチェック！

ページTOPへ