Proof and System Reliability : Proceedings of the NATO Advanced Study Institute, Marktoberdorf, Germany, from 24 July to 5 August, 2001

As society comes to rely increasingly on software for its welfare and prosperity there is an urgent need to create systems in which it can trust. Experience has shown that confidence can only come from a more profound understanding of the issues, which in turn can come only if it is based on logically sound foundations. This volume contains contributions from leading researchers in the critical disciplines of computing and information science, mathematics, logic, and complexity. All contributions are self-contained, aiming at comprehensibility as well as comprehensiveness. The volume also contains introductory hints to technical issues, concise surveys, introductions, and various fresh results and new perspectives. Front Matter....Pages i-xii Cartesian Closed Categories of Effective Domains....Pages 1-20 Algorithmic Game Semantics....Pages 21-47 Algebra of Networks....Pages 49-78 Computability and Complexity from a Programming Perspective....Pages 79-135 Logical Frameworks—A Brief Introduction....Pages 137-166 Ludics : An Introduction....Pages 167-211 Naïve Computational Type Theory....Pages 213-259 Proof-Carrying Code. Design and Implementation....Pages 261-288 Abstractions and Reductions in Model Checking....Pages 289-321 Hoare Logic: From First-Order to Propositional Formalism....Pages 323-340 Hoare Logics in Isabelle/HOL....Pages 341-367 Proof Theoretic Complexity....Pages 369-397 Feasible Computation with Higher Types....Pages 399-415

As society comes to rely increasingly on software for its welfare and prosperity there is an urgent need to create systems in which it can trust. Experience has shown that confidence can only come from a more profound understanding of the issues, which in turn can come only if it is based on logically sound foundations.
This volume contains contributions from leading researchers in the critical disciplines of computing and information science, mathematics, logic, and complexity. All contributions are self-contained, aiming at comprehensibility as well as comprehensiveness. The volume also contains introductory hints to technical issues, concise surveys, introductions, and various fresh results and new perspectives.

Perhaps the most important and striking fact of domain theory is that important categories of domains are cartesian closed.