Leanによる「文芸的プログラミング」の実装

CoqのInductiveでは定義できないinductive型を公理的に定義する方法

解析の定理証明実践＠Lean 4

Abduction Prover in Isabelle

proof irrelevance.v · GitHub

ProofSummit 2019まとめ

AI for Isabelle/HOL

Mathcompで文字列を使う

依存型の話

ニコニコをCoqで証明してみた

定理証明　＋　機械学習　＝　？

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

「The Little Prover」 の紹介

dependent types in scala

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

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