定理証明支援ツール Isabelle 上で小さな関数型言語の操作的意味論を表現し，プログラムの性質を証明します．
プログラミング言語で書かれたプログラムが表す”動作”あるいは”計算”がどのようなものであるかは，文書の中で自然言語で規定されていることが多いでしょう．ほとんどの場合はそれで充分でしょう．しかし自然言語による規定は曖昧になってしまうことがあり，あるプログラムコードがどのような動作になるのか不明確であるということが起こりえます．そのようなケースはまれかもしれませんが，検証をする人やコンパイラを作る人にとっては問題になります．
この問題を解決するためにプログラムの動作を数学的に厳密に定めるという方法があります．今回はそのような手法の1つである操作的意味論を定理証明支援ツール Isabelle で扱ってみます．小さな関数型言語を対象に操作的意味論を定め，それを使ってプログラムの性質を証明します．
初等的なレベルです．圏論の話はしません．