2011-01-07から1日間の記事一覧

インメモリDBはT-treeインデックスだから速いという話

が、 http://www.publickey1.jp/blog/09/rdb_vs.html とかに書いてあって、だからTimesTenは速いんだ、キャッシュでかい普通のRDBMSとは違うよ!って書いてある。のだけど、 http://en.wikipedia.org/wiki/T-tree には、 Although T-trees seem to be widely …

Coqで圏論

Coq

CLTT読書会で最近話題になるネタ。 ConCaT http://coq.inria.fr/pylons/contribs/view/ConCaT/v8.3 というライブラリがあるんで、これをベースにCLTTの証明なんかを書いていけば、色々よいんじゃないか的な。 ドキュメントらしいものはないけど、論文を読む…

call/cc in Lua

http://stackoverflow.com/questions/2827620/call-cc-in-lua-possible であったネタ。 前提知識(?) [1]Coroutines in Lua http://www.inf.puc-rio.br/~roberto/docs/corosblp.pdf[2]Revisiting Coroutines http://www.inf.puc-rio.br/~roberto/docs/MCC15-0…

■

A modular formalisation of finite group theory http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.122.5995 という論文を眺めたりした。CoqとCoqのライブラリであるSSReflectを使って、Feit-Thompsonの定理の証明を形式化しようという話らしい。…