[Agda] curious

[Silvio Frischknecht]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hello

I'm student at ETH Zürich. I am very interested in adga and  the theory
behind it, i.e. dependent types. However I have a hard time finding the
right literature.
I would like to learn all the things like the relation ship between
types and logic, relation to category theory, coinduction ...
I have only a very basic knowledge of these topics. I know lambda
calculus and natural deduction from my formal methods and functional
programming course but thats about it. However I'm not afraid of
abstract topics. And would also read a few paper as long as they don't
build up on to much knowledge.

Could anyone recommend me 1-2 good books about those topics?

I'm also looking for a master thesis in that field in Spring 2012. So
I'd also like to know which universities are mainly involved in
developing agda. It'd be cool if they had a student exchange agreement
with ETH.

Just as a side note I'm also interested in an internship that has
anything to do with functional programming. I just thought I'd mention
it. You never know.

Silvio
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iQIcBAEBAgAGBQJN8+L+AAoJEDLsP+zrbatWKqYQANKjX/jntW2hJX5zzIjUnDEl
4mAXW0wpOELfHX8vjzdJPIDbFY8+1ug1xBd1D/raZFTqFtP80HufmP/gxu0OPu8l
0o+Je8qC53oUljxuEWxUxv1y7Wniyms6eP7+UO7D6VcdCSmItLIQVR90hAxjdUZO
olI2aYWw26WLND9YiXQvH71ROKf13NNU/ZWTwpmJg9e0VPPcvCbVJEhsEwkWojsQ
JRDtxjFaWY3arA57rzEcB+jZpNK3QKZZPoegAMjK9Ib52Xs2H2ojR5k+B5k+nRpD
5NBou6HO5i6R9hEm15JHmDipYy2ST/+aBjq9OBo1PlXb9HCTk8WoqD87Dl5c+DlH
u/3qoQR4j/dRKeM07fQu8yY+ZwhCMTfIJdANH8nVUba/96B4NbF91K0l/jYD1nX4
rQVk/N36KB0l9lmb63wpQw2zhjkEziWqJ4T/5FjsSG9uoMYYqxGhMytq9hVOBixY
cm37Qp3iKcxRkL22tbKdneKAS3e6rTqkvsoAjcTGlG3E7R1Fs61umZ7gx1LlfIXE
wjFJImZDtm6rKpjOoZ3y+ouDRD/RdwSuK9b4j6mTKxqdTc/vVGMk+puWEkPCxnUZ
x3uB5n28SD945J4gzsTSA295vx9W4ibvBTWDJJ/UCXiQx/kbkS0l+pngFeAxUhIM
JyejF5dEY64BQcjIgg45
=ly7/
-----END PGP SIGNATURE-----