Agda

This page is obsolete!
My new page on Agda is eev-agda.html.
Old stuff:

I am learning Agda.
I am following Wadler's PLFA.
Installing it on my Debian box was difficult. My notes/instructions are here.

My plans are to implement in Agda:
1. these Natural Deduction proofs from [PH2],
2. the proto-categories from [IDARCT],
3. these constructions from [FavC],
and I also want to learn how to use this library written by Hu and Carette.