Summer Types

[Joseph Razavi]

Hi Everyone,

Now that term is over, I'm hoping to get a group going again, mostly
to work out what to do when next term starts, but also for anyone who
is around and wants to keep working through the stuff. We can probably
pick a different meeting time now that there are no timetabled
activities. If anyone is interested, let me know.

I'm also interested in hearing about people's experiences, especially
anything they think could be improved for next term.

Wishing you all thoughtful and deliberate summers,

Joe


P.S.

If anybody is really charmed by type systems and wants to do some
reading over the summer, I know of three books you can get online. All
three are hard to get an in-depth understanding of, but they might be
worth a look at if you're interested:

1) LECTURES ON THE CURRY-HOWARD ISOMORPHISM (Sørensen and Urzyczyn).
Goes into detail about how proofs in a logic can be viewed as programs
in a programming language. There is some nice background on the lambda
calculus and intuitionistic logic. Last year we read chapters 1-4 in
this reading group, and so some level of support should be available
on this list (hah!).
ftp://ftp.cs.cmu.edu/user/ftp/usr/rwh/www/home/courses/logic/www-old/handouts/curry-howard.pdf
(or ftp://ftp.mimuw.edu.pl/People/urzy/alpha.ps.Z which is the website
of one of the authors, rather than a third party, but some of you
might have difficulty with the file format.)

2) PROGRAMMING IN PER MARTIN-LÖF'S TYPE THEORY (Nordström, Petersson,
and Smith). The closest thing conceptually to what we've been doing
(though in a different system), this book studies a type theory due to
Per Martin-Löf, which is probably the most celebrated type theory
ever. In particular, it describes the key notions of inductive type
and equality type, which I hope to focus on more in our Coq adventures
in future. I kind-of understand sections 4-7 and will happily spend my
time hand-waiving and trying to read bits of logic in English --
especially with someone prepared to return the favour with section 8
if they figure it out! Peter Aczel recommended this book to me, so it
comes with good credentials.
http://www.ens-lyon.fr/denif/data/martin_lof_prog/1990/contenu/book.pdf
(or www.cse.chalmers.se/research/group/logic/book/book.ps again, this
is from the author's group's website, which you might be more
comfortable with -- but not a pdf! What is it with the cool kids and
non-pdf file formats!?)

3) INTUITIONISTIC TYPE THEORY (Martin-Löf). Covers similar ground to
(2), but is written by Per Martin-Löf himself, and with lots of nice
explanation about how it all relates to the philosophy of maths. The
way that the cartesian product and equality are defined is weird; (2)
is better for those topics and (I think!) explains the difference. I
roughly understand what's going on up to about page 79. The link below
is to a list of works on type theory; this book is the second one
down. I think the remarks next to the list items are probably worth
looking at because the material is now historical.
http://intuitionistic.wordpress.com/works-on-martin-lofs-type-theory/

Send in your own reading recommendations, and write back if you look
at any of the above. If anybody is wondering, I'd say that (3) is by
far the best as a "holiday read" !!

[Robert White]

So happy to hear the group is still on going during the summer!!!

I will be around. My internship starts on Thursday. So there is no more SE group project and computer graphics assignments. I will be able to concentrate on things like this!!!!

Big thanks for your effort for this reading group xxx.

Robert