---
date: "2023-08-22T23:39:29+0900"
---
#tools #software #programming-language #logic

[[依存型]]に基づいた定理証明支援システム。フランス[[INRIA]]で開発され、プログラムの正当性証明に使用される。

[[Coqの勉強]]で学習リソースを整理している。

### 関連研究者

- [[Emilio Jesús Gallego Arias]] - [[Faust]]の形式的証明プロジェクトに関わっている