THE SEMANTICS OF INTUITIONISTIC AND CLASSICAL PROOFS
This chapter gives an account of the semantics of intuitionistic natural deduction proof, based on models of the simply-typed lambda-calculus. A new form of games semantics is introduced that forms the basis for a running example throughout the study. This new form combines features of the games of Lorenzen used to model intuitionistic provability, and of the games used by Hyland and Ong to interpret fragments of linear logic, and Ong to interpret terms of the lambda-mu-calculus. The semantics of classical natural deduction proofs is presented via recently-developed models of the lambda-mu-calculus, and its disjunctive extensions based on fibrations of models of simply-typed calculi. Continuations are also considered in this context, adumbrating some of concerns in later chapters.
Oxford Scholarship Online requires a subscription or purchase to access the full text of books within the service. Public users can however freely search the site and view the abstracts and keywords for each book and chapter.
If you think you should have access to this title, please contact your librarian.