プログラミング好きの備忘録

関数型言語とか、証明とか

夏期休暇にやりたいこと

やるべきことがあるときに限って、そうじゃないことが捗る… 試験前の掃除、とか。

発端を忘れてしまいましたが、気になる単語からリンクを飛んでいった結果、やりたいことが浮かび上がってきました。


圏論の本を読む
途中挫折の可能性もありますが、とにかく触れてみるべき
きっかけはもちろんHaskellです


・カリーハワード同型対応
本や論文があったら読んでみる
これは、証明駆動に関連した話題。


・Certified Programming with Dependent Types (Adam Chlipala)
依存型による、証明されたプログラミング(直訳)
pdfにして350ページ超の文献
Coqに関する話。


・Hoare論理
部分的正当性の表明(という言い方を見ました。)
事前条件、事後条件
これは手が出るかどうかわからないのでメモ程度に。


・Types and Programming Languages (Benjamin C. Pierce)
型付きラムダ計算についての知識を広げたい。
大学の図書館に置いてあったので二ヶ月前に借りたが、厚すぎて時間が取れず、挫折(あと英語)
いきなりこれで入るのではなく、入門用の本があるかもしれないので調べてみる。



英語の本を読むときには一度に全部読もうとすると死にそうなので重要な部分に絞るべき?
そのへんのテクニックをまず調べる