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

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

2007-11-05から1日間の記事一覧

セマンティクス

(*****************************************) (** SEMANTICS *) (*****************************************) Require Import List. Section ListAssoc. Variable A B:Set. Variable A_beq : A -> A -> bool. Fixpoint List_assoc (l:list (A*B))(a:A){str…

シンタクス

(*****************************************) (** SYNTAX *) (*****************************************) (** 基本データ構造を二分木構造で定める *) Inductive DATA:Type := | DNIL : DATA | DCONS : DATA -> DATA -> DATA. Inductive VAR : Type := | …

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

とってもシンプルな言語をCoq内で定義してみた。次のような感じでプログラムは表現される。 (* プログラムの例 入力された2数を足し算するプログラム *) Definition plus_program := MAIN ( X O 詳細は以下