[Agda] Request of suggestion of learning material for Agda

[Martin Escardo]

On 27/08/17 20:48, 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.

"Dependent types at work" by Bove and Dybjer is an excellent starting 
point.

http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf

Martin


> 
> 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.
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe