60年代後半にホーアはプログラムの挙動について推論するための論理体型を導入し、プログラム検証の形式化の道を切り開きました。その論理体系はホーア論理と呼ばれ、現在も様々な形で拡張されてプログラムの検証に用いられています。こうした中、ホーア論理のモデルを構築するにはプログラミング言語の意味論に現れるモナドと呼ばれる数学的構造を意識すると見通しが良くなることがわかってきました。本講演ではモナドを通じたホーア論理のモデルに関する研究成果についてお話します。