[Agda] Request of suggestion of learning material for Agda

[Harley D. Eades III]

Hi, Mario.

A very nice starting point might be the following book by Aaron Stump:

https://www.amazon.com/Verified-Functional-Programming-Agda-Books/dp/1970001240

It has been used in the undergraduate programming languages course at the
University of Iowa several times.

Best,
Harley

> On Aug 27, 2017, at 3:48 PM, Mario Castelán Castro <marioxcc.MT at yandex.com> wrote:
> 
> Hello.
> 
> I want to learn computer programming and proof formalization in Agda. I
> am aware that there are *several* tutorials listed in
> <http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials>.
> Listing several tutorials adds the difficulty of choosing among them.
> 
> Obviously I do not want to read from an obsolete tutorial, but since it
> is necessary to *already* know the current Agda to tell whether a
> tutorial is current, I am instead writing to the members of this mailing
> list to ask for a specific suggestion. A suggestion to read a book or
> manual instead of tutorial is also welcome.
> 
> In case it makes any difference, I want to mention that I am familiar
> with classical propositional and first order logic, and to a lesser
> degree, ZF set theory and HOL4. I do not have any experience with
> dependent types.
> 
> I am willing to read a book about type theory in parallel with
> Agda-specific material if this is required.
> 
> Regards.
> 
> --
> Do not eat animals, respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 801 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170827/7383b71e/attachment.sig>