Table of Contents

PrefaceAcknowledgements1. Typefree lambda-calculus2. Intuitionistic logic3. Simply typed lambdacalculus4. The Curry-Howard isomorphism5. Proofs as combinators6. Classical logic and control operators7. Sequent calculus8. First-order logic9. First-order arithmetic10. Gödel's system T11. Second-order logic and polymorphism12. Second-order arithmetic13. Dependent types14. Pure type systems and the lambda-cubeA Mathematical BackgroundB Solutions and hints to selected exercisesBibliographyIndex