430 B
430 B
date
| date |
|---|
| 2023-08-22T23:39:29+0900 |
#tools #software #programming-language #logic
依存型に基づいた定理証明支援システム。フランスINRIAで開発され、プログラムの正当性証明に使用される。
Coqの勉強で学習リソースを整理している。
関連研究者
- Emilio Jesús Gallego Arias - Faustの形式的証明プロジェクトに関わっている