[Agda] curious

[Anthony de Almeida Lopes]

After the various Agda introductions, I would recommend "The Power of
Pi." I wish I had known about it sooner on in my Agda usage.

2011/6/12 Danel Ahman <danel.ahman at eesti.ee>:
> Hi SIlvio,
>
>
> The Agda wiki seems to have a couple of introductory papers on Agda from Ulf Norell ,Peter Dybjer, Ana Bove and others (http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials). It should also be worth to look at Ulf Norell's PhD thesis to get some background behind Agda.
>
> In addition, it is worth looking at a couple of reasoning courses based on Agda. Thorsten Alternkirch has given such a course in Nottingham (http://www.cs.nott.ac.uk/~txa/g53cfr/) and there is also Conor McBride's course with video lectures given in Edinburgh (http://homepages.inf.ed.ac.uk/s0894694/agda-course/).
>
> You should also be able to find interesting details about dependently typed programming from numerous Epigram papers (e.g. Why Dependent Types Matter by Alternkirch and McBride). More details and background can be found if the references from these papers are followed.
>
>
> Best regards,
> Danel Ahman
>
>
>
> On 12.06.2011, at 0:49, Silvio Frischknecht wrote:
>
>> -----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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>