[Coq] TAPL Chapter 8

TAPL Chap.8 の演習問題をCoqで証明しました。型があるのでChap.3より寧ろ楽かも。

http://ideone.com/ttTKY

[TAPL][OCaml] Untyped Lambda Calculus Interpreter

　TAPLのChap.5を読むのに型無しλ計算のインタプリタが無いかなと探していたところ下記を見つけました。（...まぁそもそもそのくらい自分で作れよ、という話はあるんだが）

http://www.cs.ru.nl/~freek/notes/lambda.ml

ページの内容を lambda.ml として保存し、

$ ocaml
# #use "lambda.ml";;

で読み込まれるので、あとは下記の様に試すだけ。

# nf "(^x.fx)a";;
- : term = term "fa"
# nf "(KISS)(KISS)";;
- : term = term "^yzz'.zz'(yzz')"
# red_gk all "SKK";;
- : term list =
[term "SKK"; term "(^yz.Kz(yz))K"; term "^z.(^y.z)(Kz)"; term "^z.z"]
# red 7 "(^x.xx)(^x.xx)";;
- : term list =
[term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx";
 term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx";
 term "(^x.xx)^x.xx"; term "..."]
#

手計算に自信が無い時に使うといいかなー。

[TAPL][Coq] Chapter 3: Boolean Expression

TAPLのChapter 3のBoolean式の部分に付いてCoqで証明してみました。
コードは http://ideone.com/COzSO に公開しています。

[TAPL] Types and Programming Languages Reading at Tokyo

Types and Programming Languages (通称 TAPL) の読書会の第0回が先日あったので報告。

TAPL読書会ですが、下記の様にGoogle groupが出来ました。開催情報とか流れるので興味のある方は登録をお勧めします。
http://groups.google.co.jp/group/taplreading-tokyo
次回開催は 11/3午後で、会場は同じく豆蔵オフィスです。

前回は、Chap.1はスキップ、Chap.2から読み始め、Chap.3の途中まででした。
次回はChap.3の続きから初めて、Chap.4(というか実装のChapterはこの先も)はスキップ、Chap.5を読む予定、となっています。
参加者は予習復習前提で、次回の範囲は予め読んで来ることが前提と、硬派な勉強会ということになりました。
Chap.4のような実装の箇所は各自実装したい人が自分で実装してちょっとデモをするということで。

参加者ですが、前回は総勢４名もCS専攻の大学院生の方が来てくれたのは良かったです。素人の社会人だけで勉強会してると簡単に行き詰るので。

懇親会も大変盛り上がっていたようで、大変有意義な一日でした。しかし、積読率高いですね＞TAPL。買ったけど読んでなかったとか、Chap.3までは読んだけどとか、そういう話ばっかり。