依存型の話
ニコニコをCoqで証明してみた
定理証明 ＋ 機械学習 ＝ ？
無条件に仮定にFalseを追加して、どんなサブゴールも消せるtactic作ったよ
「The Little Prover」 の紹介
dependent types in scala
JAXA/IPA クリティカルソフトウェアワークショップ 言語系発表とその後(今朝の版)
WOCSにおける言語系（一部自動車、安全を含む）発表一覧、このうちの特徴的なものの紹介資料作成中
SAT/SMTソルバの仕組み
ATS/LF for Coq users
