Lambda to pi
I gave a talk a while back which included an interpreter for the pi-calculus, and a compiler from the lambda-calculus to it. I didn't really do justice to the material in a few slides, so here's a proper blog post. This article is available as a Literate Haskell file, which you can load into GHCi directly. The π-calculus If the λ-calculus is a minimal functional language, then the π-calculus is a
full-sessions-0.6.1 - keigoiの日記
full-sessionsの新バージョン 0.6.1 を HackageDBにアップロード しました。 full-sessions は、Haskellにおけるマルチスレッド/ネットワークプログラミングのライブラリです。 Sessionモナドという新しいモナドを使ってプログラムを書きます。 チャネルの型表現にπ計算の型理論の一つであるセッション型を採用しています。セッション型のおかげで、チャネルの「使われ方（プロトコル）」がスレッド間で整合していることを実行前の型検査によりチェックできます。これにより、ある種のデッドロックや型の不整合は型検査で排除できるようになります。 さらにHaskellの型推論でセッション型を推論させれば、プログラムがチャネルを意図通りに使っていることを型表現からチェックできます。 full-sessions は、HList等で見られるような型レベルプログラミングのテク
Haskell 型レベルプログラミングの DSLへの応用 id : keigoi (OCaml-Nagoya) HAMA.jp 2009 1 発表の構成 1. ドメイン特化言語と Haskell 2. 型クラスとFunDeps基礎 3. FunDepsによる型レベルプログラミング 4. ドメ��
Haskell 型レベルプログラミングの DSLへの応用 id : keigoi (OCaml-Nagoya) HAMA.jp 2009 1 発表の構成 1. ドメイン特化言語と Haskell 2. 型クラスとFunDeps基礎 3. FunDepsによる型レベルプログラミング 4. ドメイン特化言語「セッション型」による ネットワークプログラミング 2 ドメイン特化言語 (Domain Specific Language) • 各領域で、そこに特化した言語(DSL)がデザイ ンされてきた。 • データベースアクセス ... SQL • ハードウェアデザイン ... Verilog • システム制御 ... 微分方程式とブロック線図 3 DSLはわかりやすい • DSLでプログラムを書けば、 • もっとも短く • もっとも簡潔に • もっともわかりやすく ソフトウェアを構成できる (少な
full-sessions : yet another implementation of session types in Haskell
full-sessions : yet another implementation of session types in Haskell by Keigo IMAI @ Nagoya University if you find any bugs please send an email to the above address. any other comments are also appreciated. download (rev. 181, June 25, 2009) for GHC 6.8 or above feature full functionality of session types (types for communication protocols over channels) including branching recursion (bas
セッション型の分岐 - keigoiの日記
セッション型を備えた 「型付きErlang」みたいなのがあればいいのになあ、と思うんですが(ある？)、一から型推論やら多相性やらを作り上げるのは面倒でしょうしHaskellやMLよりも便利で安全な型システムなんてあろうはずもないので(ぉぃ)、私たちはHaskellでセッション型を使いましょう。 今回はセッション型における「分岐」について説明します． セッション型の分岐 と 分岐ラベル セッション型における分岐は，通信の両端点が同じように分岐することを保証する．このように通信プロトコルに沿った分岐を実現するには，「どちらに分岐したか」という情報をやりとりする必要がある． 私の現在の実装では，分岐を表現するために「ラベル」を受け渡す．ここでラベルは '1' または '2' のどちらかである．(もっと複雑な分岐は この2分岐のネストで表現できる．) チャネル k を介してラベル 1 を送る操作を
セッション型 on Haskell - keigoiの日記
セッション型は プロトコルを表現する型で， 15年くらい前から π計算の型理論の1つとして研究されてきました(文献リスト(一部))．並行・分散ソフトウェアの普及を鑑みるに，セッション型のような仕組みは次世代の型安全かつ表現力の高いプログラミングのための強力なツールとして役に立つと考えます． しかしその直観的なわかりやすさにも関わらず，セッション型を提供しているプログラミング言語は皆無(おそらく…)です． そこで，今 流行(?)の型レベル計算を駆使して Haskell にセッション型を導入してみました． ダウンロード 晒してみる． まだ α版 full-sessions ダウンロードページへ test.hs を ghci でロードしてください いくつかの関数は 型を見たり runS で走らせたりできます． test.hs の一部で ixdo 記法を使っているので， cabal install
PiMonad - a network programming framework based on Pi-Calculus
PiMonad - a network programming framework based on Pi-Calculus What is PiMonad? PiMonad is a library for functional programming language Haskell. Points are : Lightweight implementation of the Pi-Calculus, a process algebra with channel-passing feature. Network programming framework equipped with channel-passing feature. (Future work) Design with Pi-Calculus, verify it, then implement it with PiMo
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
pi-calculus