ICFP 2010 実況など
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
d.y.d. - ICFP 2010
22:27 10/10/06 ICFP 2010 International Conference on Functional Programming に行ってきました。 Haskell や OCaml や Scheme や Erlang 等々「関数型プログラミング言語」の研究の国際会議です。 延々と twitter で実況つぶやきしてたのを ICFP 2010 実況など にまとめましたので、どんな発表があったのか興味のある方は、そちらをどうぞ。 自分にとって特に面白かった！というベスト３は、この三つかなあ。 VeriML: typed computation of logical terms inside a language with effects 「証明を書けるプログラミング言語」は素晴らしいのですけども、 そんなに大変でないように思える証明でも、書くと、想像以上に長くなってしまう
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
プログラミング言語 Misa
#! /usr/bin/misa ごっ、ごぉおっ、ご〜きげんよおぉおおぉおほっ。ほおぉおぉおっ。 「ごきげん☆みゃぁああ”あ”ぁ”ぁああ〜っ」 さわやかな朝の☆ご挨拶！ お挨拶がっ。 澄みきった青空にこだましちゃうぉ〜ああぉおおおぉん。 「は、はひっ、はろおぉっ☆わぁるどおおぉっぉ〜っ」 こ、この文章は☆おサンプル！ おおぉおぉおおサンプルプログラム！！ どんなおプログラム言語でも基本のご挨拶させていただくのぉぉおッ！ 「ぽうっ」 長々と書くのがこ、ここでの〜、ここでのぉおおぉおぉぉおたしなみぃぃいぃ。 「長いぃ。長すぎましゅう。ご挨拶にこんなプログラム長すぎまひゅぅうぅ☆ んおおぉぉ、ばかになる、おばかになっちゃいましゅ〜ッ」 長いのがっ、バッファの奥まで入ってきましゅたぁあぁあっ！ ばっふぁ☆溢れちゃいまひゅぅ〜。あみゃぁあ”あ”ぁ”ぁああ”あ”ぁぁ。 「で
Rietveldでレビューしよう @ val it: α → α = fun
This entry was posted by Jun Mukai on Friday, 25 December, 2009 本当はいろいろ実地で試してから文章を書こうかと思ったんだけど、まあ、just an ideaということで。 Rietveldってたぶん、聞いたことがある人はプログラミング系の人以外にはないと思うのだけど、これって本とかの内容チェックなどにも普通に便利なんじゃないかなーと思う。そんなわけで、今回はRietveldっていうのがどういうもので、どういう問題を解決し、なぜ本とかのレビューにも向いているかという話をしたい。 Rietveldというのはコードレビュー用のシステムだ。GoogleではMondrianという名前のコードレビューシステムが使われている。これを外部でも使いたいということで、Mondrianの作者が作ったのがRietveldである(コードが共有されてるの
d.y.d.おもしろいみろん
13:33 08/06/29 RSS of kmonos/wlog moved! http://www.kmonos.net/wlog/index.rdf いや、移動したのは15ヶ月前なので、すでにご存じの方は華麗にスルーしてください。 「ここのRSSが文字化けしてるよー」という方だけ、↑に登録変更していただけると、 直るかと思います。お手数おかけしてスミマセン。定期的に「文字化けってる」という 指摘を見かけるので再度ブロードキャストです。こう、辛辣な評議会とかで怒られそうですけど、 諸般の事情により古い方からリダイレクトかけるの難しいらしいのだよね… それはそうと、昨日の記事に追記しました。 10:26 08/06/28 Logic ∩ CS 検索してたらたまたまヒットした "On the Unusual Effectiveness of Logic in Computer Scienc
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
