COQ

Coqは証明支援システムの一つ。Coqの核はプログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所の[http://www.pps.univ-paris-diderot.fr/pi.r2/ PI.R2]チーム([http://www.pps.univ-paris-diderot.fr PPS]研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。[http://pauillac.inria.fr/~herbelin/ Hugo Herbelin]が事実上の開発代表者である。