OCamlを使ったシステム開発まとめ - osiire’s blog
うちの会社(有限会社ITプランニング）でやってきたOCamlを使ったシステム開発の概要を書いておきます。ふと思うと今までまとめて公開したことはなかったなと。別に隠す程のものじゃないし、もしこれからOCamlを使ったプロジェクトを始めてみたい人の参考になれば嬉しいです。 2006年 某証券会社のWebサービスの一部を担当 株価を解析して、その結果をWebAPIとして提供。OCaml + MySQL。HTTPベースで提供されるXMLファイルが生データだったので、この時初めてXMLのパースにxml-lightを使った。これはかなり便利。その後も使い続けている。nc(network cat)ライクなモジュールも作った。行列変換のためにC言語との連携もしたけど、特に問題なし。そういえば、この頃はmarshalingが好きで、DBへmarshalingデータをそのまま保存して「Objectデータベース
今日のCoq: 型づけ規則とそれに関する補題 - みずぴー日記
とうとう、型づけ規則の定義ができました。 というわけで、簡単な補題を証明しようとしたところ、string_decがうまく扱えなくて挫折しました。 証明したかった補題はTAPLに載っている「Inversion of the typing relation」という補題です。TAPL曰く、Immediate from the definitionらしいです。 (* typing t tenvは、型環境tenvにおいてtが型づけ可能ならSome type、型がつかないならNoneを返す。 *) Lemma InvTypeRelVar : forall (tenv : list (string * type)) (x : string) (r : type), Some r = typing (Var x) tenv -> In (x,r) tenv. というわけで証明にチャレンジします。 まずは、
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
