メモ
今はまだ理解できないことについても，時間の余裕ができたとき，なんとなくそっち系の気分になったときや，気合を入れて体系的に学ぶ必要に迫られたときのために，メモを残しておく心がけは大事だと思う．
そういう意味では「世界に」公開された日記を使うのは無意味に恥ずかしいのでアレだが，妙なプライドに基づく悪い意味での完璧主義をなくす薬になるかもしれない*1．
- http://www.andrew.cmu.edu/user/cebrown/notes/hindley97.html J. Roger Hindley, Basic Simple Type Theory. Cambridge University Press, 1997. （書評というか概要）
- wikipedia:"Curry-Howard"
- http://www.pps.jussieu.fr/~krivine/articles/Wollic05.pdf The Curry-Howard correspondence in classical analysis and set theory
- http://nicosia.is.s.u-tokyo.ac.jp/pub/staff/hagiya/kougiroku/vs/kensho.ppt 自動証明・検証技術
- http://nicosia.is.s.u-tokyo.ac.jp/members/hagiya.html てか萩谷先生のトップページ
↑もうちょっとカテゴリごとにまとめてくれればいいのに...
- http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ Isabelle
- http://nicosia.is.s.u-tokyo.ac.jp/pub/essay/hagiya/essay/keishikika 形式化願望
- http://e-learn.mine.nu/mizar/jordancurve.htm JORDAN曲線定理の完全証明が完成！
- http://www.ags.uni-sb.de/~omega/workshops/TheoremaOmega05/talks/brown.pdf Foundations of Grundlagen
- http://www.cs.ru.nl/~freek/ Freek Wiedijk （形式化ヲタ）
- http://web.cs.ualberta.ca/~piotr/Mizar/mirror/http/ Mizar
- googleScholar:"concurrent garbage collection"
- citeceer:"concurrent garbage collection"
- http://citeseer.ist.psu.edu/futamura99partial.html Partial Evaluation of Computation Process An Approach to a Compiler-Compiler
- http://www.brics.dk/RS/00/44/BRICS-RS-00-44.pdf The Second Futamura Projection for Type-Directed Partial Evaluation
- http://compose.labri.fr/documentation/pe/pe_resources.php3 Partial Evaluation - Resources
- http://citeseer.ist.psu.edu/consel93partial.html Partial Evaluation: Principles and Perspectives
二村研サイトで書誌情報を探そうと思ったら，いつの間にか消滅していた．武市研の先輩曰く「もう退官なさったよ」ぇーー．ついこないだまであったのに... （こないだっていつだ？） けっこう長くて，ちょっと古めかしいPDF（確か二村先生本人のもの）を昔ACM Digital Libraryから（学校で）落としたのだが，そのときはよく分からなくて消してしまった．それが分からなくなった．
666 名前：デフォルトの名無しさん[sage] 投稿日：2005/12/12(月) 14:43:52
これすごいな。そんなの実現可能なの？
ヒープ使わないとなるとデカイ静的メモリ領域用意して全部つっこむしか思いつかない俺に喝を入れてくれ。668 名前：654[sage] 投稿日：2005/12/12(月) 14:51:51
私もちゃんとは知らないウロ覚えの聞きかじりなんだが、
何年か前に日本ソフトウェア科学会のとある研究集会あたりで聞いたような気がする。
私の気が確かならば関数型プログラミング方面から来た話で、
プログラムを解析（エスケープ解析とかあたりかなぁ）して
関数呼び出しの階層の中の適切な階層に記憶管理コードを埋め込むような話が あったような気がする。
ただ3時から仕事上の講演会を聞きに行くので今は調べられない。
戻ってきた後でちょっとググって見る。669 名前：654[sage] 投稿日：2005/12/12(月) 15:11:16
PPL2003の招待講演だったNe（希ガス）
http://www.csg.is.titech.ac.jp/ppl2002/program.html
"Functional Programming without Garbage Collection"
Martin Hofmann (University of Muenchen)
[PSファイル]
http://www.csg.is.titech.ac.jp/ppl2002/proceedings/hofmann.ps670 名前：654[sage] 投稿日：2005/12/12(月) 15:13:10
ちなみに内容はウロ覚えなんで論文読んで確認されたし。
(聞きに行く講演は15時半からだった。)671 名前：666[sage] 投稿日：2005/12/12(月) 16:03:54
トンクス！
なるほどね。ヒープを使わずに再帰しながらスタックを使う（関数の引数に詰め込む）ってことっぽい。
672 名前：654[sage] 投稿日：2005/12/12(月) 18:37:12
ま、それを手でやったら単に面倒なだけなんだけど
プログラムを解析して自動でそういうように書き換えるって話だったように覚えるんだけど
どうだったかいね。
（最近PDFが多くて生PSのみってあんまりないから今使ってるマシンに
PSプロセッサを入れてないのでURLの論文をまだ読んでない罠。
や、まぁ入れりゃいいだけなんではあるがマンドクセぇという。）いくらAppel様とは言え20年前の論文だから，はっきり言って今 役に立つかどうか怪しい．テスト環境に使った，特殊なプロジェクトで作られた "Massive Memory Machine" とやらが持ってるRAMが128MBだったり．やはりあのGC本を読むべきなのか．でも達成すべき目標が未達成の今，GCは優先度低いんだよな．やっぱスーパースカラー，SIMDとかキャッシュとかの方面を... そう，情報収集だけで実装のできない自分を鍛え直すという目標を忘れてはいけない．ていうかAppel読み終えてないし．
- http://llvm.cs.uiuc.edu/pubs/2005-02-TECS-SAFECode.html Memory Safety Without Garbage Collection for Embedded Applications
- http://www.cs.princeton.edu/~appel/papers/45.ps Garbage Collection Can Be Faster Than Stack Allocation
- http://www.cs.kent.ac.uk/people/staff/rej/gc.html Richard Jones's Garbage Collection page
