証明駆動開発入門(2) 上記ページの勉強メモです。 Extraction coq から OCaml, Haskell, Scheme のコードを出力する。 OCaml にコードを出力するにはそのまま Extraction map. とすればいい。 これで (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **…

証明駆動開発入門(1) 何かを読む会 という社内勉強会が発足されました。 読んだ本の内容を共有しよう。 一人で勉強していてもダレるので共有することで無理やり進捗を出そう。 他の人の発表を聞いて読んだ気になろう。 っていう緩めの会です。 途中まで読ん…