定理証明　＋　機械学習　＝　？

無条件に仮定にFalseを追加して、どんなサブゴールも消せるtactic作ったよ

「The Little Prover」 の紹介

dependent types in scala

JAXA/IPA クリティカルソフトウェアワークショップ　言語系発表とその後(今朝の版)

WOCSにおける言語系（一部自動車、安全を含む）発表一覧、このうちの特徴的なものの紹介資料作成中

SAT/SMTソルバの仕組み

ATS/LF for Coq users