Kon*_*tov 29 type-systems theorem-proving agda
我正在努力学习agda.但是,我遇到了问题.我在agda wiki上找到的所有教程对我来说都太复杂了,涵盖了编程的不同方面.在阅读了关于agda的3个教程之后,我能够编写简单的证明,但我仍然没有足够的知识将它用于真正的单词算法正确性.
你能推荐我关于这个主题的任何教程吗？类似于学习自己一个Haskell,但对于Agda.
小智 21
大约一年前,当我开始学习Agda时,我想我尝试了所有可用的教程,每个教我一些新东西.
您应该尝试一下Coq,因为它拥有更大的用户群,并且有两本可用的好书:
软件基础也非常好.
好的是,Agda和Coq所基于的理论有些相似,所以很多例子可以从一个转换成另一个.Martin-Löf类型理论中的编程是依赖类型理论的一个非常好的和可读的介绍,它可以为你清除一些东西.
了解"真实世界算法"是什么意思会有所帮助.在提到Agda的论文中描述了许多示例开发.