I haven't had the chance to watch the two videos yet, but at BFPG (2015-03), Matthew Brecknell did an "<i>Introduction to Agda</i>" talk that might also be interesting to some.<p><a href="https://www.youtube.com/watch?v=QyUVONbwHYE" rel="nofollow">https://www.youtube.com/watch?v=QyUVONbwHYE</a><p><a href="https://www.youtube.com/watch?v=7iAkFh9xOIc" rel="nofollow">https://www.youtube.com/watch?v=7iAkFh9xOIc</a>
If you’re interested in learning Agda, you might want to check out Conor McBride’s courses, given at the University of Cambridge:<p>“Introduction to dependently typed programming using Agda”, 2011:<p><a href="http://www.cl.cam.ac.uk/~ok259/agda-course/" rel="nofollow">http://www.cl.cam.ac.uk/~ok259/agda-course/</a><p>Course materials:<p><a href="https://github.com/mietek/agda-introduction" rel="nofollow">https://github.com/mietek/agda-introduction</a><p>“Dependently typed metaprogramming (in Agda)”, 2013:<p><a href="http://www.cl.cam.ac.uk/~ok259/agda-course-13/" rel="nofollow">http://www.cl.cam.ac.uk/~ok259/agda-course-13/</a><p>Course materials:<p><a href="https://github.com/pigworker/MetaprogAgda" rel="nofollow">https://github.com/pigworker/MetaprogAgda</a>
Agda, Coq etc is something I really want to learn someday. I'm already pretty proud that I finally can write some haskell, but this stuff is next level. I might give Idris a go first though, as it seems very similar to haskell in syntax.