Today's Session and Other activities

[Joe Razavi]

Hi,

As Giles correctly remembered, today we're sticking with chapter 2, to
give people a chance to get to grips with the material before we move
on.

Since several of you who once seemed keen are no longer following, I
wonder whether it is worth running a catch-up session so that people
can enjoy the rest of the reading even if the lambda calculus section
went too fast. Write back with thoughts.

Finally, now we've seen Intuitionistic Logic it's time for me to
arrange some Coq "labs" for anyone interested. If anyone would like to
see how Coq works, let me know when you are free -- eventually I'll
invite everyone in CS/Maths to come, but I want to set the time to
prioritise reading group members.

There are several reasons one might want to learn Coq. It's an
interesting and well-regarded example of a theorem prover, it has a
mature program extractor which demonstrates the correspondence between
computer science and logic, and there are communities of real
mathematicians who use Coq for their real research!

See you soon,

Joe