[Agda] curious

[Anthony de Almeida Lopes]

Oh and for type theory in general it seems everyone reads "Types and
Programming Languages." I haven't and went with the books "Proofs and
Types" by Jean-Yves Girard and "Practical Foundations for Programming
Languages" by Robert Harper.

Because of this, my education on the operational aspects of TT are
rather spotty. I'm currently looking for further supplemental
material. I'm thinking "Type Checking and Normalisation" by James
Maitland Chapman may be what I missed out on but I have not started in
on it yet.

Anyone have any recommendations? I'd rather not start over with TAPL,
not that review is bad, just that review this soon after the others
seems rather boring.


2011/6/12 Guillaume Yziquel <guillaume.yziquel at gmx.ch>:
> Le Sunday 12 Jun 2011 à 12:30:58 (+0100), Conor McBride a écrit :
>> Hi
>>
>> As a matter of record, Why Dependent Types Matter is by
>> Altenkirch, McBride and McKinna.
>
> Not exactly Agda-related, but I find "Certified Programming With
> Dependent Types" to be quite a good read.
>
>        http://adam.chlipala.net/cpdt/
>
> --
>     Guillaume Yziquel
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>