[Agda] curious

[Anthony de Almeida Lopes]

Another book that really cleared some things up in ML-TT for me is,
"Programming in Martin-Löf's Type Theory"

http://www.cse.chalmers.se/research/group/logic/book/

It's only 211 pages and very easy to read.

"Type Theory and Functional Programming" by S. Thompson is another
free one. It explains all of the basic and more advanced formations
with a very Curry-Howard isomorphism perspective. Be warned though, if
you order the original from CafePress, it will have a lot of typos.

http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/


2011/6/11 Silvio Frischknecht <silvio.frischi at gmail.com>:
> -----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-----
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>