以前から僕は単相の型推論アルゴリズムの健全性や完全性をCoqで検証していたのですが，最近*1let多相をサポートするように型推論器の実装と正当性の証明を修正したので記事にしておきましょう*2． *1:と言っても今年の1月ぐらいですが．本当はAdvent Calenda…