Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings (Q1416071)

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 0997.00025). Indexed articles: \textit{Abrial, Jean-Raymond; Cansell, Dominique}, Click'n prove: interactive proofs within set theory, 1-24 [Zbl 1279.68283] \textit{Norrish, Michael}, Complete integer decision procedures as derived rules in HOL, 71-86 [Zbl 1279.68292] \textit{Magaud, Nicolas}, Changing data representation within the \textsf{Coq} system, 87-102 [Zbl 1279.68290] \textit{Slind, Konrad; Hurd, Joe}, Applications of polytypism in theorem proving, 103-119 [Zbl 1279.68296] \textit{Schürmann, Carsten; Pfenning, Frank}, A coverage checking algorithm for LF, 120-135 [Zbl 1279.68295] \textit{Kapur, Deepak; Sakhanenko, Nikita A.}, Automatic generation of generalization lemmas for proving properties of tail-recursive definitions, 136-154 [Zbl 1279.03034] \textit{Cachera, David; Pichardie, David}, Embedding of systems of affine recurrence equations in \textsf{Coq}, 155-170 [Zbl 1279.68286] \textit{Amjad, Hasan}, Programming a symbolic model checker in a fully expansive theorem prover, 171-187 [Zbl 1279.68284] \textit{Cruz-Filipe, Luís; Spitters, Bas}, Program extraction from large proof developments, 205-220 [Zbl 1279.68287] \textit{Wiedijk, Freek; Zwanenburg, Jan}, First order logic with domain conditions, 221-237 [Zbl 1279.68299] \textit{Reed, Jason}, Extending higher-order unification to support proof irrelevance, 238-252 [Zbl 1279.68294] \textit{Krstić, Sava; Matthews, John}, Inductive invariants for nested recursion, 253-269 [Zbl 1279.68289] \textit{Théry, Laurent}, Proving pearl: Knuth's algorithm for prime numbers, 304-318 [Zbl 1279.68298] \textit{Meikle, Laura I.; Fleuriot, Jacques D.}, Formalizing Hilbert's Grundlagen in Isabelle/Isar, 319-334 [Zbl 1279.68291]