https://twitter.com/kinaba のログ (twilog の方が便利です。)
Boostのドキュメントって、なんでこんなに、どのヘッダをincludeすれば使えるのかわかりにくいのが多いんだろう… | |
おもしろい問題だ http://twitter.com/s01/status/21375206236 | |
109999.99999999 というのはできた。もっと増やすには… | |
SevenTrees をずっと考えている。普通に再帰をバンバンつかって(iso T nat)∧(iso nat (nat*nat))経由で証明しちゃうぜー、と思ってやり始めたんだけどこれはこれで意外とめんどいな。nat→Tの停止性とかに証明が要る。元問題に忠実に再帰なしを考えよう | |
Sevenといえば、自宅の最寄りのセブンイレブンが改修工事だかなんだかで閉まっているのでトマトゼリー http://twitter.com/kinaba/status/20645547061 が入手できない。危機的状況である | |
@yoshihiro503 (1.1-1.3/1.2) ではなくて (1.2-1.3/1.1) でやってました>約11万 | |
Ackermann http://as305.dyndns.org/aps/problem/view/14 Coqのリファレンスのサイトが落ちてて問題解けないので、易しい問題を増やしましょう月間です | |
@kmizu ちょっとお値段が高めですが、僕は結構好きです。ケチャップともトマトジュースとも違う方向性のトマト味で、なかなか良い感じ。 | |
@pirapira おおお!ありがとうございます!また時間が @kikx さんに奪われる! | |
日記書いた http://www.kmonos.net/wlog/112.html#_2026100817 あなぷらーを増やそう | |
@tana_ash http://ja.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E6%89%8B%E6%B3%95#.E8.87.AA.E5.8B.95.E8.A8.BC.E6.98.8E 自動証明/モデル検査 とかの方向はどうですか。現状は、保守的すぎ(問題ないプログラムでもコンパイルエラーにしちゃっ)たり、正常動作することの証明を大量に人間が手書きしなきゃいけない部分も多いですが。 | |
@tana_ash Windowsのドライバ開発キットについてくるSDV http://www.microsoft.com/japan/whdc/devtools/tools/sdv.mspx http://research.microsoft.com/en-us/projects/slam/ なんかは結構大々的に使われている気がします | |
知らなかった http://twitter.com/MoCo7/status/20362515446 ぐぐらびりてぃ下がってね?と思ったら既にかなり上にいるなぁ。すごい | |
ロブ=グリエって亡くなっていたのか…。『迷路のなかで』 途中で挫折したのをいつか再挑戦しようと思っていたはずが、随分時間が経ってしまった。 |