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

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.