[Agda] Request of suggestion of learning material for Agda

[Aaron Stump]

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.
Best,
Aaron

On Sun, Aug 27, 2017 at 6:44 PM, John Leo <leo at halfaya.org> wrote:

> My recommended sources for learning type theory, Agda, and related topics:
> https://github.com/halfaya/BayHac/blob/master/references.md
>
> 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.
>
> John
>
> On Sun, Aug 27, 2017 at 3:27 PM, Harley D. Eades III <
> harley.eades at gmail.com> wrote:
>
>> 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
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170827/6a904319/attachment-0001.html>