[Agda] Request of suggestion of learning material for Agda

John Leo leo at halfaya.org
Mon Aug 28 01:44:53 CEST 2017


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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170827/e42ca675/attachment.html>


More information about the Agda mailing list