CODEWITHSUNDEEP
type-systemstheorem-provingagda
Konstantin Solomatov
Konstantin Solomatov

Reputation: 10352

How to learn agda

I am trying to learn agda. However, I got a problem. All the tutorials which I found on agda wiki are too complex for me and cover different aspects of programming. After parallel reading of 3 tutorials on agda I was able to write simple proofs but I still don't have enough knowledge to use it for real word algorithm correctness.

Can you recommend me any tutorials on the subject? Something similar to Learn Yourself a Haskell but for Agda.

Upvotes: 32

Views: 5424

Answers (3)

jimmy
jimmy

Reputation: 148

Here are some additional resources as of 2022.

  1. Programming Language Foundations in Agda: This book was written in the style of Software Foundations but using Agda instead of Coq. The author taught a course using Software Foundations and wrote a blurb explaining why they decided to rewrite the book in Agda.

  2. Notes on PLFA: These are a set of notes that serve as commentary to PLFA. The author also wrote the well-regarded book...

  3. Logic and Computation Intertwined: While not an Agda book per se, it introduces proof assistants first through the construction of your own small proof assistant (written in Racket). The book also contains a section on Agda.

  4. Learn You An Agda: A shorter text but helpful to skim through.

Upvotes: 2

wjedynak
wjedynak

Reputation: 421

When I started learning Agda about a year ago I think I tried all available tutorials and each taught me something new.

You should probably give Coq a try, because it has a larger user base and there are two nice books available for it:

  1. Coq'Art - slightly dated, but beginner friendly
  2. Certified Programming with Dependent Types

Software Foundations is also very nice.

The nice thing is that the theories Agda and Coq are based on are somewhat similar, so many examples can be translated from one to another. Programming in Martin-Löf's Type Theory is a really nice and readable introduction to the dependent type theory, it can clear some things for you.

It would help to know what do you mean by "real world algorithms". Many example developments are described in papers which mention Agda.

Upvotes: 23

Necrototem
Necrototem

Reputation: 554

Conor McBride gave a great series of lectures last year on dependently-typed programming using Agda. It's a good place to go if you want a break from pouring through terse tutorials on the topic. I believe there are also accompanying exercises.

Upvotes: 20

Related Questions