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