Coqが今流行っているらしい。twitter経由で偶然ハノイの塔をCoq形式化している記事を見つけた。 なんか巷でCoqがはやっているようなので - 菊やんの雑記帳なんかおもしろそうなので一つ簡単な命題を証明してみた。証明したこと Lemma answer_length : forall…

OCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket…

ocaml-nagoyaのプログラミング合宿に参加してきました。一泊二日で長野の麻績(おみ)に行って、鍋も食べ、焼肉も食べ、酒も飲み、コーディングもして、発表もするというハードなスケジュールでしたが、久しぶりにocaml-nagoyaのメンバーにも会えて非常に充実…

Coq version 8.2以降からHaskell風の型クラスが使えるようになったから使ってみることにした。Haskellで型クラスといえばMonadが有名な気がするのでHaskell風のモナドHMonadを定義しよう。Coqでの型クラスは次のように宣言するみたいだ。 Class HMonad (M: T…

OCaml Meeting に行ってきました。 id:camlspotterさんid:osiireさんid:keigoiさんharreさんid:mzpさんid:Gemmaさんそしてid:zyxwvさんおつかれさまでした。OCaml入門者向けから、上級者向けまでさまざまな講演があって非常に楽しめました。OCamlという言語…