Agda
https://upload.wikimedia.org/wikipedia/commons/thumb/7/71/Agda%27s_official_logo.svg/800px-Agda%27s_official_logo.svg.png
定理証明系言語
依存型がある
Coqより「プログラミング言語っぽい」
SyntaxはHaskellっぽい
homepage
github
Haskell実装
入門
https://github.com/khibino/DTPiA-read
https://twitter.com/khibino/status/1381055552600465412
https://qiita.com/bra_cat_ket/items/bb8c385736b16ad046cd
http://ie.u-ryukyu.ac.jp/~e115763/slides/events/osc2014/slide.html
https://www.slideshare.net/ussopyon/ss-43846794
AgdaのコードってめっちゃUnicode出てくるんやなmrsekut.icon
ref
code:agda
instance
import Categorical.Raw as C
open ≈-Reasoning
open import Relation.Binary.PropositionalEquality hiding (sym; refl)
logicH : LogicH _⇨_ _↠_ q
logicH = record
{ F-false = Fₘ-f∘ε≈β∘f false
; F-true = Fₘ-f∘ε≈β∘f true
圏論
http://www.ie.u-ryukyu.ac.jp/~kono/lecture/software/Agda/index.html
https://github.com/TOTBWF/agda-category-theory-exercises
https://github.com/agda/agda-categories
https://github.com/copumpkin/categories
https://github.com/conal/denotational-hardware
表示的ハードウェア？
_<_>_という関数
https://twitter.com/notogawa/status/1335850559169941505
参考
http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/intertheodraft2.pdf
https://en.wikipedia.org/wiki/Agda_(programming_language)
https://qiita.com/karrym/items/138313a0904708e38889
https://qiita.com/karrym/items/351e4bf3f8072555bc52
https://qiita.com/karrym/items/0d3ba2aad108390d19fe
https://qiita.com/karrym/items/c7f26f54563550d1256b
http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
https://www.slideshare.net/ussopyon/agda-45453544
型推論器の定式化
https://ja.wikipedia.org/wiki/Agda
#プログラミング言語