×

zbMATH — the first resource for mathematics

Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20–23, 2002. Proceedings. (English) Zbl 0997.00025
Lecture Notes in Computer Science. 2410. Berlin: Springer. x, 349 p. (2002).

Show indexed articles as search result.

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

MSC:
00B25 Proceedings of conferences of miscellaneous specific interest
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Software:
Coq
PDF BibTeX XML Cite