kinaba @kinaba #WMM Appelの招待講演：静的解析器で不変条件を挿入→（以下Coqで）検証→公理的意味論から操作的意味論から双模倣で証明しやすい操作的意味論からLeroyのCompCertで抽象マシン語にコンパイルしてからPPCへ、という、並列性を扱えるCコンパイラツールチェインについて。 2010-09-25 23:39:52 kinaba @kinaba #WMM システムコールやpthreadはオラクルとして抽象化してやる。"この量の証明は機械化証明なしでは無理"、"証明のモジュール化(module,依存型,型クラス)重要"/(感想)それでもまだモジュール化機構が"足りてない"感を感じるけど証明言語は将来どうなるかなー 2010-09-25 23:50:59
完全にド素人なわけで、どうせほとんど何言ってるかわからんのだろうなぁと思ってたんですが、意外とわかるものももあったので書いておこうかと。わかると言っても、どうやってやったかとかまではなかなかわからんくて、モチベーションくらいがわかればそれだけでも嬉しいという幸せな話でして。 プロシーディングはここにあるみたいだ。 http://portal.acm.org/toc.cfm?id=1596550&coll=portal&dl=ACM&type=proceeding&idx=SERIES824&part=series&WantType=Proceedings&title=ICFP&CFID=505049525&CFTOKEN=505049525 以下、たぶん間違ってたりそんなことは重要なことではないということを書いてたりします。 Organizing Functional Code for P
http://www.icfpcontest.org/ 疲れた…。 今年はまあ何というか、孤独との戦いであった。 来年はちゃんと休みをもらって、ちゃんとチームを作って出たいと思った。 初日はkzk氏、hillbig氏とともになんかやってました。 今年は問題がシンプルだなと思った。 時間制限3時間とかのICPCのJava Challengeとかよりもはるかにシンプルなのですけど。 そして、問題の制約が恐ろしく緩い。 どこまで想定すればいいのでか。 そして、Windows版が用意されないシミュレータ。 アメリカ語を2時間ぐらい掛けて頑張って読んで、 適当にプロトコルかいたりしてたら、 開始4時間後ぐらいには愚直ダッシュコントローラができてたような気がする。 しばらくしてナイーブな敵と穴避けアルゴリズムが完成して、 すでに与えられたマップが終わってしまった。 しばらくしてMLにスコア自慢が現れて
ICFP Contest 2008 « lambda.oasis :: cpoucet -> content
For those that are unaware, in exactly one month the 3 day ICFP contest will be held again. This contest has been held for 10 years already and has seen a steady increase in participants, especially in the last two years. Curiously, this ties in with my previous post as it seems that this contest has reached critical mass in 2006 to become really big in 2007. For those wondering what the contest i
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
