Home page and stuff
Jan Malakhovski
The main contribution of which is a reworked seminar plan.
Some comments:
I thought about it and came to the conclusion that it might be a bit
harsh to start from Agda right off the bat.
Thus, I think we shall
* start from untyped lambda, proving all the properties by hand,
* write an interpreter for it in itself, defining datatypes on the way,
* write an interpreter for it in Agda (should be helpful for those
without Haskell experience),
* learn how to prove equality lemmas in Agda,
* and finally, try to prove some of the properties of untyped lambda in Agda.
"Datatypes" list item should probably be redistributed between other
items above from it, but I'm not sure how to do this yet.
Also, I'm not sure if we should crunch all the non-type-theory topics
(logic systems, algebraic semantics, arithmetic systems and etc) in a
one go or spread it somehow (like in "Lectures on Curry-Howard
Isomorphism" by Sorensen and Urzyczyn).
Currently it's distributed like this: "type theory - related non type
theory - type theory again - ..."
Also, check the public_fs/ttfv.
Objections, suggestions, comments?
Andrew Shulayev
Andrew Shulayev
Jan Malakhovski
"Lectures on Curry-Howard Isomorphism" (1998/2006 doesn't matter)
* 1998th year version is available from here:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385
* In any case: Agda tutorials.
On Tue, Apr 17, 2012 at 12:39 AM, Andrew Shulayev <shul...@rain.ifmo.ru> wrote:
> What are we supposed to read before meeting on this Thursday?
>
> Andrew Shulayev
>
> --
> You received this message because you are subscribed to the Google Groups "Type Theory for Vegetables" group.
> To post to this group, send email to type-theory-f...@googlegroups.com.
> To unsubscribe from this group, send email to type-theory-for-veg...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/type-theory-for-vegetables?hl=en.
>