こんにちは。4回生の uda / @t_uda です。院試やばい院試やばい。
第 4 回 TAPL*1読書会の報告です。諸事情により予定していた日に読書会ができなかったため、第 4 回までおよそ 1 ヵ月程間が空いてしまいました。
実装章は各自でやってもらうことにしてサクサク進めて前回までで Part I の内容が終わったので、今回から Part II, Ch.8 "Typed Arithmetic Expressions" に入りました。簡単な型が導入されて、ようやく "Types" っぽい話題になってきました。
内容としては、型付け可能の定義に始まり、 well-typed terms が持つ良い性質（safety など）を、型の導出に関する帰納法を用いて証明しました。単純な型しかないので割と簡単な証明ばかりでしたが、導出に関する帰納法に慣れてない人にはちょうど良いプラクティスになると思います。
次回 Ch.9 から単純な型付きλ計算を扱っていくので、これからどんどん面白くなりそうです。…が、夏休みに入ってしまうので次の読書会は大分先になりそうです。
*1:Types and Programming Languages
