generated at
Coq
定理証明系言語
INRIAが開発
もともとは型システムにCalculus of Constructionsを使っていた
その略称「CoC」が言語名の由来
Thierry CoquandとGérard Huet
というかCoCの実装として作られたのがCoq?
1991年以降はというCalculus of Inductive Constructions型システムを用いている
Christine Paulin-Mohring


github
HP

install
https://coq.inria.fr/opam-using.html
instller
https://github.com/coq/coq/releases

チュートリアル
https://www.iij-ii.co.jp/activities/programming-coq/coqt1.html
http://proofcafe.org/sf/
http://herb.h.kobe-u.ac.jp/snap/coq.pdf
これが良いらしい
https://qiita.com/kaizen_nagoya/items/13566f0b2083ea8d4998
めっちゃある
https://qiita.com/tnagao7/items/d44f683bfdc5eb297466
/layerx/Coq


Coqban


Coqを用いて解かれた数学の問題
四色定理

https://github.com/FreeProving/free-compiler
haskell→coqのコンパイラ

https://www.youtube.com/watch?v=GYCTpBitVMA


型クラス
https://qiita.com/yoshihiro503/items/a6fe93ae0d867129f7b1
http://yosh.hateblo.jp/entry/20090904/p1
https://m-hiyama.hatenablog.com/entry/20150118/1421547031
https://blog.7nobo.me/2017/02/11/120000.html
https://blog.7nobo.me/2017/02/10/120000.html
https://blog.7nobo.me/2017/02/09/155706.html

https://github.com/pirapira/coq2rust
coqからrustを生成する

正規表現
https://fetburner.hatenablog.com/entry/2020/12/03/222042


タクティック
https://keigoi.hatenadiary.org/entry/20100104/1262584662
https://keigoi.hatenadiary.org/entry/20091229/1262096861


Logical Foundations
https://softwarefoundations.cis.upenn.edu/
https://zehnpaard.hatenablog.com/entry/2021/04/01/090643

https://github.com/coq/coq/wiki/TheoryBehindCoq
https://ncatlab.org/nlab/show/Coq
https://employment.en-japan.com/engineerhub/entry/2018/08/10/110000
https://m-hiyama.hatenablog.com/entry/20141207/1417948454
http://awm.jp/~yoya/docs/sfja/toc.html
https://fetburner.hatenablog.com/entry/2020/05/28/194451
https://staff.aist.go.jp/tanaka-akira/pub/2018-09-02-deptype-proofsummit2018.pdf
https://fetburner.hatenablog.com/entry/2020/12/05/000024
https://mathlog.info/articles/1405
https://zehnpaard.hatenablog.com/entry/2021/04/12/081526
https://www.slideshare.net/yoshihiromizoguchi/coq-52677439?utm_source=pocket_mylist
https://www.wantedly.com/companies/wantedly/post_articles/402992
https://myuon-myon.hatenablog.com/entry/2017/04/16/195944

#プログラミング言語