これは Haskell Advent Calendar 2011 の5日目の記事です。 去年も書きましたが、その記事はこちら → Haskell厨を6年やってる俺がOCamlを仕事で2ヶ月使ってみた - keigoiの日記先日の記事 Haskell＋タグレスな型付きDSLで楽々！C言語コード生成 - keigoiの日…

VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るの…

論文でました EPTCSというオンライン論文集に私の論文が掲載されました。 指導教員の先生との共著になっています。 Session Type Inference in Haskell WOCS9で発表します 第９回クリティカルソフトウェアワークショップ (WOCS9) @ パシフィコ横浜 (11/17木-…

関数型プログラミング言語とコード生成 HaskellやOCamlなどはコンパイラなどの言語処理系の実装を得意としている。さすがに日常的にコンパイラを実装している人はそう多くないと思うけど、例えばコード自動生成はすぐ試せる割に効き目が大きく、仕事を効率化…

ついに、Alloy を使って完全な λ計算 (β簡約) を表現できた…。（前回 は中途半端だった。） なかなか面白いのは、Alloy がうまくノードを使って無駄なくβ簡約しているところ（Ω=(λx.xx)(λx.xx) で Ω→Ωなど。後に載せる）。(8/22)フレーム条件のバグを直した…

フォロー記事あり前回 (Alloyでλ式をつくる) では、λ式を表現するグラフをAlloyで構築した。 今回は、λ計算の核となるβ簡約の一部をAlloyで記述してみる。 扱えるλ式の制限 面倒だったので、モデルに次の制限を導入した。 このため、正確にはβ簡約とはいいが…

Alloyでλ式を作ってみた。 フォロー記事あり あまり役に立たない気はするけど、関係の逆(~)を取ったり(反射)推移閉包(*,^)を使う良い練習になった。（バグがみつかり次第、色々修正している。以下のモデル図はソースを修正しながら作っているので、エンバグ…

前回は、線形型をもつ DSL の例として 線形λ計算を挙げ、実装を示した。 これをもっと押し進めれば、ファイルやネットワーク接続などのリソースの「使い方」をより詳しく指定できる DSL をエンコードできるはずだ (きれいに書けるか、使う人が居るかは別問題…

線形λ計算というのは、「変数をちょうど一度だけ使わなければならない」という線形型をもったλ計算だ。これを Haskell で実装してみた。「ファイルが開かれたら必ず閉じる」という制約のような、線形型 (linear type) が必要な DSL の実装の参考になるかもし…

分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。 具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これ…

Alloyの言語仕様をゴリゴリ読み進めていた。 非常に勉強になります。Software Abstractions (1st ed., p.288): So although a quantified constraint with multiple declarations may be regarded, for some quantifiers, as a shorthand for nested constra…

Androidで動作するOCamlインタプリタ OCaml toplevel on Android を Android Market に公開しました。 OCamlのトップレベル(インタプリタ)をAndroid上で操作できます。 enjoy! 仕組み OCamlトップレベルはネイティブ実行されます(OCamlバイトコード+libcamlr…

pa_monad は OCamlで モナドを使いやすくするための構文拡張だ． ついこの前 id:camlspotter さんが pa_monad の拡張を書いてくださった．ありがたや． 早速使ってみようと思い，コンパイルした．hg clone https://bitbucket.org/camlspotter/pa_monad_custo…

O'Caml on Android というパッチを作っている． 柔軟かつ信頼性の高いOCamlでAndroidのアプリを書くのが目標だ． ここ2ヶ月ほどocamljs (OCamlからJavaScriptへのコンパイラ) を使っていて、OCamlの信頼感と柔軟性にとても満足したので，ではAndroidでもOCam…