6 Resources

The resources listed on this page are not required for the course, but may prove useful.

The Agda wiki contains links to information about Agda, but it can be a little difficult to find what you need. As with many wikis, some pages are out of date or skeletal.

Systems similar to Agda include Isabelle/HOL, Nuprl, Lean, and the dependently-typed programming languages Twelf, Coq, and Idris.

My CS 798 course web site contains links for resources using Coq, if you want to learn more about that.

My flânerie Logic and Computation Intertwined takes the reader through the construction of a small proof assistant in Racket, before quick introductions to Agda and Coq. All of this takes place within the framework of learning propositional and predicate logic (the material was originally used by me for the course CS 245E). There are suggestions for further reading there which may be of interest to you.