30分プログラム、その717。最近、functionalなキューばかり作っていたので、普通のキューも作ってみました。 ま、Perlだから配列にpushしてshiftするとキューになるんですけどね! せっかくなので、オブジェクトっぽくしておきました。 使い方 my $q = Queue-…

Coqでラムダ計算を証明してみた - みずぴー日記の続けて、単純型付きラムダ計算の型推論(Type reconstruction)に関する定理の証明をしてました。そして、とうとう健全性と完全性の証明ができました! やったね! GitHub - mzp/lambda at c0123fd0ca42d545f9e45…