Coq - mrsekut-p

Coq

定理証明系言語

INRIAが開発

もともとは型システムにCalculus of Constructionsを使っていた

その略称「CoC」が言語名の由来

Thierry CoquandとGérard Huet

というかCoCの実装として作られたのがCoq?

1991年以降はというCalculus of Inductive Constructions型システムを用いている

Christine Paulin-Mohring

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

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

#プログラミング言語