Coqでつくる手続き型プログラミング言語

とってもシンプルな言語をCoq内で定義してみた。

次のような感じでプログラムは表現される。

(* プログラムの例 入力された２数を足し算するプログラム *)
Definition plus_program :=
MAIN (
   X O <- LEFT (!X_IN);                  (*変数X_INの左値を変数X0に代入*)
   X_OUT <- RIGHT (!X_IN);               (*変数X_INの右値を変数X_OUTに代入*)
   WHILE (!X O) (                        (*変数X0がnilになるまでループ*)
      X_OUT <- CONS (D DNIL) (!X_OUT);   (*X_OUTに(nil, X_OUTの値)を代入*)
      X O <- RIGHT (!X O)                (*X0にX0の右値を代入*)
   )
).

詳細は以下