This volume contains elaborations of the lectures given at the Marktoberdorf Summer School 2003 on “Proof Technology and Computation”, the 24th of a series of Advanced Study Institute sponsored by the NATO Scientific and Environmental Affairs Division.

Nowadays, “Proof technology” will become an established field in software engineering. It generally aims at integrating proof processing into industrial design and verifications tools. The origins of this technology lie in the systematic understanding of a fully-fledged, precise notion of proof by mathematics and logics. Using this profound understanding computer scientists are able to implement proofs, to check and create them automatically and to connect the concepts of proof and programs in a deep way. Via this, connection proofs are used to support the development of reliable software systems. Software engineers have integrated proof processing into industrial development tools, and these implementations are now getting very efficient. The Summer School 2003 at Marktoberdorf gave a detailed and profound overview on actual researching results and its industrial application around this proof technology.

Robert Constable lectured on the benefits and technical challenges of sharing formal mathematics among interactive theorem provers. The goal of Gilles Dowek was to present classical results on proof normalization for various axiomatic theories using a newly proposed formulation of predicate logic, called deduction modulo, where a theory is defined by a set of axioms and rewrite rules. Orna Grumberg presented an abstraction-refinement framework of temporal logic model checking, which has then been extended to deal with 3-valued abstraction, game-based model checking and full CTL.

John Harrison demonstrated, that formal verification is an increasingly important topic in industrial hardware design. He gave a broad overview of the main techniques currently being used for industrial-scale hardware verification with special attention to the construction of interactive theorem provers using the “LCF” approach. Highlights of several important topics concerning relations between the theory of computability and computational complexity on the one hand, and programming languages on the other were presented by Neil D. Jones. Tobias Nipkow lectured on readable machine-checked proofs and semantics, based on Isabelle/HOL and Isar, as well as the application of this theorem proving framework to the specification and analysis of operational semantics for Jinja, a Java-like language.

The lecture series from Michael Rathjen were concerned with an intuitionistic and predicative theory of types developed by Martin-Löf and a constructive version of Zermelo-Fraenkel set theory inaugurated by Myhill and further developed by Aczel. Helmut Schwichtenberg has shown the important point in exact real numbers, as opposed to floating point numbers and to develop the basics of real analysis in such a way that from a proof of an existence formula one can extract a program. Pawel Urzyczyn lectured on predicates as types. The covered issues were related to the Curry-Howard Isomorphism for predicate logic, including first-order intuitionistic logic and arithmetic.

Moshe Y. Vardi's course provided an introduction to the theory of automata on infinite objects and demonstrates its applications to design specification, verification, and synthesis. The automata-theoretic approach to design verification uses the theory of automata as a unifying paradigm. Stanley S. Wainer lectured fundamental ideas from mathematical logic and proof theory, connecting the computational complexity of recursions with the logical complexity of their termination-proofs.

The Summer School has been two weeks of learning, discussing and developing new ideas, and a gainful event, both from the professional and from the social aspect. Again, the Summer School benefited a lot from the experienced scientific staff from Munich and the local Marktoberdorf crew. Our sincere thanks go to all of them.

The Editors