読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

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

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

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

(* プログラムの例 入力された2数を足し算するプログラム *)
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の右値を代入*)
   )
).

詳細は以下