ソフトウェアの基礎

単純型付きラムダ計算(Simply Typed Lambda-Calculus, STLC)は、 関数抽象(functional abstraction)を具現する、小さな、核となる計算体系です。 関数抽象は、ほとんどすべての実世界のプログラミング言語に何らかの形 (関数、手続き、メソッド等)で現れます。 ここでは、この計算体系(構文、スモールステップ意味論、 型付け規則)とその性質(進行と保存)の形式化を、 これまでやったのとまったく同じパターンで行います。 (扱うためにいくらかの作業が必要になる)新しい技術的挑戦は、 すべて変数束縛(variable binding)と置換(substitution)の機構から生じます。 STLC は基本型(base types)の何らかの集まりの上に構成されます。 基本型はブール型、数値、文字列などです。 実際にどの基本型を選択するかは問題ではありま

[VoQn]

STLC、単純型付きラムダ計算の解説および実装演習 (Coqで)