■ - ひとり勉強会
ここ「ひとり勉強会」は、会と言いつつひとりで勉強した記録を残してます。 金曜日は YARV: Yet Another Ruby VM のソースコード読みの日です。 履歴 (1): main から yarv コアに到達するまで (2): コンパイル処理の流れとデータ構造 (3): if のコンパイル (4): case, while のコンパイル (5): break, next, redo, retry, rescue, ensure, for, ブロック のコンパイル (6): 代入 のコンパイル (7): 自己代入, メソッド呼び出し のコンパイル (8): super, yield, リテラルなどなど のコンパイル (9): def, class, module, alias などなど のコンパイル ここまでのまとめ: PPT or PDF (10): 最適化 (11): バイトコー
■ - ひとり勉強会
ここ「ひとり勉強会」は、会と言いつつひとりで勉強した記録を残してます。 Coq の解説記事を書くために勉強しています。 (1): forall A B: Prop, (A->B) -> A -> B. CoqIDEのつかいかた。forall と -> の証明。 (2): forall A B: Prop, ~(A ∨ B) -> (~A ∧ ~B). and と or と not の証明。Inductive な命題。 (3): forall n: nat, exists m, (n=2*m ∨ n=2*m+1). 自然数やリスト。再帰的 Inductive なデータ。= と 帰納法 と exists の証明。omega, ring, field による自動証明。標準ライブラリの使い方。 (4): 解説テキストリンク集 (番外編): VSTTE 2012 Software Verificat
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
