3 Nov 2002 chalst   » (Master)

raph: Two points:
  1. If you don't check that the translation is good, then there is every chance that either:
    • the proofs you carry out in your rich system do not correspond naturally to proofs in Z_2;
    • your rich system does not share the same consequence relation as Z_2;
    (btw I use SOA and Z_2 interchangeably to mean `a reasonable axiomatisation of the usual SOA consequence relation').
  2. I can't say what the best books are, since I picked up most of what I know from fairly obscure sources. The text I have read that gives the best feel of what life is like in a a proof theory based on the lambda calculus is Jean-Yves Girard's `Proofs and Types' (with appendices by Paul Taylor and Yves Lafont). This text gives many of the most important results, in particular the proof of strong normalisation for System F and Martin-Loef's demonstration that this SN result is equivalent to the consistency of SOA, but be warned that this text is challenging, cavalier about definitions and has a very non-mainstream agenda. Also the book does not explain why polymorphism is not set-theoretic; for this I recommend John Reynold's orginal paper.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!