<div dir="ltr"><div>Hi, all.  Sorry if the price of my book is high -- I have no input or control of that, as it is all determined by the publisher.  One good thing is that many universities subscribe to ACM Books as part of their subscription to the ACM Digital Library, and then the book is free to read online through that subscription (I believe the same is true if you have your own subscription to the ACM DL).  Students in my class get the book completely free (electronic version) that way.<br></div><div>Best,<br></div>Aaron<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Aug 27, 2017 at 6:44 PM, John Leo <span dir="ltr"><<a href="mailto:leo@halfaya.org" target="_blank">leo@halfaya.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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" target="_blank">https://github.com/halfaya/<wbr>BayHac/blob/master/references.<wbr>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><span class="HOEnZb"><font color="#888888"><div><br></div><div>John</div></font></span></div><div class="HOEnZb"><div class="h5"><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/Verifie<wbr>d-Functional-Programming-Agda-<wbr>Books/dp/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="m_-5107772738940857056h5"><br>
> On Aug 27, 2017, at 3:48 PM, Mario Castelán Castro <<a href="mailto:marioxcc.MT@yandex.com" target="_blank">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.s<wbr>e/agda/pmwiki.php?n=Main.Other<wbr>tutorials</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" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</div></div><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>