Quick
index
main
eev
maths
blogme
dednat6
littlelangs
PURO
(GAC2,
C3TD,
λMDetc)
(Chapa 1)

emacs
lua
(la)tex
fvwm
agda
tcl
forth
icon
debian
irc
contact

Agda

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.