<div dir="ltr">My recommended sources for learning type theory, Agda, and related topics:<div><a href="https://github.com/halfaya/BayHac/blob/master/references.md">https://github.com/halfaya/BayHac/blob/master/references.md</a><br></div><div><br></div><div>Stump's book is like an easier version of Software Foundations, using Agda.  Since it is so expensive and SF is free, I recommend going through the latter and trying to solve the exercises in Agda.  This requires some amount of sophistication with Agda already.  It is a very worthwhile exercise, both for learning Agda and comparing it to Coq.</div><div><br></div><div>John</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Aug 27, 2017 at 3:27 PM, Harley D. Eades III <span dir="ltr"><<a href="mailto:harley.eades@gmail.com" target="_blank">harley.eades@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi, Mario.<br>
<br>
A very nice starting point might be the following book by Aaron Stump:<br>
<br>
<a href="https://www.amazon.com/Verified-Functional-Programming-Agda-Books/dp/1970001240" rel="noreferrer" target="_blank">https://www.amazon.com/<wbr>Verified-Functional-<wbr>Programming-Agda-Books/dp/<wbr>1970001240</a><br>
<br>
It has been used in the undergraduate programming languages course at the<br>
University of Iowa several times.<br>
<br>
Best,<br>
Harley<br>
<div><div class="h5"><br>
> On Aug 27, 2017, at 3:48 PM, Mario Castelán Castro <<a href="mailto:marioxcc.MT@yandex.com">marioxcc.MT@yandex.com</a>> wrote:<br>
><br>
> Hello.<br>
><br>
> I want to learn computer programming and proof formalization in Agda. I<br>
> am aware that there are *several* tutorials listed in<br>
> <<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials" rel="noreferrer" target="_blank">http://wiki.portal.chalmers.<wbr>se/agda/pmwiki.php?n=Main.<wbr>Othertutorials</a>>.<br>
> Listing several tutorials adds the difficulty of choosing among them.<br>
><br>
> Obviously I do not want to read from an obsolete tutorial, but since it<br>
> is necessary to *already* know the current Agda to tell whether a<br>
> tutorial is current, I am instead writing to the members of this mailing<br>
> list to ask for a specific suggestion. A suggestion to read a book or<br>
> manual instead of tutorial is also welcome.<br>
><br>
> In case it makes any difference, I want to mention that I am familiar<br>
> with classical propositional and first order logic, and to a lesser<br>
> degree, ZF set theory and HOL4. I do not have any experience with<br>
> dependent types.<br>
><br>
> I am willing to read a book about type theory in parallel with<br>
> Agda-specific material if this is required.<br>
><br>
> Regards.<br>
><br>
> --<br>
> Do not eat animals, respect them as you respect people.<br>
> <a href="https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan" rel="noreferrer" target="_blank">https://duckduckgo.com/?q=how+<wbr>to+(become+OR+eat)+vegan</a><br>
><br>
</div></div>> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>