generated at
Agda
定理証明系言語
依存型がある
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
ref
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


#プログラミング言語