Some links

http://www.math.ucla.edu/~joan/
http://www.math.ucla.edu/~joan/gvfjrmeng.pdf

http://www.math.ucla.edu/~ynm/papers.htm
http://www.math.ucla.edu/~ynm/papers/eng.pdf

On 2 October 2012 08:58, <

Thanks for those stimulating suggestions for reading -- I just enjoyed
(skim) reading them. I have to say I thought both were a little
advanced, at least for beginning material.

At the meeting yesterday, there was some agreement with a thought of
mine that perhaps the book we were reading before really was the best
introduction to the Curry-Howard Correspondence we were likely to
find.

In light of that, I think it´s best to spend only the remaining week
casting about for alternative ways of treating the same subject
directly. Then next time we could decide what to do, it seems the
options are:

1) Do the same material again, but perhaps with a different emphasis.
Or else find similar material (Andrea suggested looking for
summer-school courses). I have to say that while material such as the
first of George´s links is definitely high quality (and fascinating if
you have time to read it), it is mostly concerned with the
nitty-gritty of constructive mathematics, which I think is a bit of a
scary subject. My own efforts so far at finding mateiral like that
have been similarly advanced. It´s a shame that the Troelstra article
( http://www.informatik.uni-ulm.de/ki/Edu/Vorlesungen/Typentheorie/SS98...
) referred to in George´s suggested reading doesn´t cover all of the
rules of a natural deduction system for  intuitionistic propositional
calculus (see part 3, beginning at the bottom of page 239).

2) Cover the same ground, but in a more ¨hands on¨ style. We could do
intuitionistic logic entirely via Coq, and type theory in a suitable
functional programming language (i.e. one where the isomorphism would
be reasonably easy to see). Someone suggested a possible author to
read I think in that vein -- please reply, I think you´re either Jonas
or Francis, or a linear combination.

3) Read a larger variety of CS theory, focussing on shorter, more
accessible reading. I think this might actually work out best of all,
allowing participants to miss sessions without dropping behind. I sort
of promised to suggest some reading of this sort.

That´s all for now (I don´t think I´m happy enough with any of the
possible reading I´ve found so far on the topic of IPL to post any
links, though you might enjoy Dummet´s perpective on constructive
mathematics in the bit of
http://www.amazon.ca/Elements-Intuitionism-Michael-Dummett/dp/0198505...
that amazon let you read for free.)

Joe

(P.S. The Moschovakis paper George links is certainly one I like to
get to understand in the next three years, although to be honest it´s
been on my personal ¨probably too scary to try¨ list since I saw it!)

On 3 October 2012 15:56, George Curtis <gdc...@gmail.com> wrote: