http://kantei.rw.to/mixi 他人の結果を覗き見するためにプロフィール経由せず、id指定して、鑑定結果を見れるようにしてみた --to compile,ghc -package network main.hs import Network.Socket import Network.BSD import IO(catch) hoge :: Integer -> IO…

Functional Programming and Parallel Graph Rewritingという本がWeb上で公開されてた。Cleanの本なのかどうかは分からないが、とりあえず、chapter7を読むと、 ・flat/non-flat domainの定義が分かる ・Abstract Reductionがなんか分かった気になる という…

Coqとかに比べて、Sparkleユーザって、世界に10人くらいしかいなそうなので(いや知らんけどね)、なんかもうナンバー1よりオンリー1って感じだよな〜(何が一応マニュアルっぽいものはあった。マニュアルというには、アレだが http://www.cs.kun.nl/~marko/res…

主にSparkleのソースを読むときに、型の表記がよくわからんのがキモイということで調べた。他はまあ、Haskell分かれば、(書けるかどうかは知らんが)とりあえず、読めるかな〜と ・基本型 Int,Bool,Char,Real・一意型 型の前に、*を付けると一意型。一意型は…

http://alohakun.blog7.fc2.com/blog-entry-614.html この日記のタイトルは、半角スペースかなんかだった記憶が。こことかで、ソース見ると、ちゃんと半角スペースになってるような。というわけで、ノータイトルじゃないんです＞＜>L.L. Ring そ･･･それくら…

証明からプログラムを抽出するという研究は、そこそこ昔からあるらしい(し、Coqなんかで実際に実装されてもいる)けど、逆はないのかな。あんまし原理的なことが理解できてないんで、あれなんだけども、formal proof書くのは、プログラム書くのの500倍(当社比…