Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20--23, 2002. Proceedings (Q701699)

The articles of mathematical interest will be reviewed individually. The preceding conference (14th, 2001) has been reviewed (see Zbl 0971.00027). Indexed articles: \textit{Butler, Ricky}, Formal methods at NASA Langley, 1-2 [Zbl 1013.68735] \textit{Huet, Gérard}, Higher order unification 30 years later (Extended abstract), 3-12 [Zbl 1013.68541] \textit{Ambler, Simon J.; Crole, Roy L.; Momigliano, Alberto}, Combining higher order abstract syntax with tactical theorem proving and (co)induction, 13-30 [Zbl 1013.68545] \textit{Barthe, Gilles; Courtieu, Pierre}, Efficient reasoning about executable specifications in Coq, 31-46 [Zbl 1013.68539] \textit{Basin, David; Friedrich, Stefan; Gawkowski, Marek}, Verified bytecode model checkers, 47-66 [Zbl 1013.68544] \textit{Bauer, Gertrud; Nipkow, Tobias}, The 5 colour theorem in Isabelle/Isar, 67-82 [Zbl 1013.68200] \textit{Bertot, Yves; Capretta, Venanzio; Barman, Kuntal Das}, Type-theoretic functional semantics, 83-98 [Zbl 1013.68114] \textit{Brucker, Achim D.; Wolff, Burkhart}, A proposal for a formal OCL semantics in Isabelle/HOL, 99-114 [Zbl 1013.68538] \textit{Courant, Judicaël}, Explicit universes for the calculus of constructions, 115-130 [Zbl 1013.68540] \textit{Dawson, Jeremy E.; Goré, Rajeev}, Formalised cut admissibility for display logic, 131-147 [Zbl 1013.03011] \textit{Dehlinger, Christophe; Dufourd, Jean-François}, Formalizing the trading theorem for the classification of surfaces, 148-163 [Zbl 1013.68195] \textit{Delahaye, David}, Free-style theorem proving, 164-181 [Zbl 1013.68196] \textit{Dennis, Louise A.; Bundy, Alan}, A comparison of two proof critics: Power vs. robustness, 182-197 [Zbl 1013.68537] \textit{Felty, Amy P.}, Two-level meta-reasoning in Coq, 198-213 [Zbl 1013.68201] \textit{Gordon, Michael J. C.}, PuzzleTool: An example of programming computation and deduction, 214-229 [Zbl 1013.68542] \textit{Hurd, Joe}, A formal approach to probabilistic termination, 230-245 [Zbl 1013.68193] \textit{Mayero, Micaela}, Using theorem proving for numerical analysis. Correctness proof of an automatic differentiation algorithm, 246-262 [Zbl 1013.68203] \textit{Nogin, Aleksey}, Quotient types: A modular approach, 263-280 [Zbl 1013.68198] \textit{Nogin, Aleksey; Hickey, Jason}, Sequent schema for derived rules, 281-297 [Zbl 1013.68199] \textit{Prevosto, Virgile; Doligez, Damien; Hardin, Thérèse}, Algebraic structures and dependent records, 298-313 [Zbl 1013.68194] \textit{Schneider, Klaus}, Proving the equivalence of microstep and macrostep semantics, 314-331 [Zbl 1013.68197] \textit{Zhang, Xingyuan; Munro, Malcolm; Harman, Mark; Hu, Lin}, Weakest precondition for general recursive programs formalized in Coq, 332-347 [Zbl 1013.68202]