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

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

OCaml

OCamlでlet recを使わずにfact関数を定義する

今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうか…

OCamlerのためのCoq便利モジュールを公開してみた

このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。ダウンロード: http://sourceforge.jp/projects/coqbase/具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を…

OCaml合宿に行ってきた

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

OCaml Meeting と FLTV に行ってきました。

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