LEADER 04591nam 22007575 450 001 9910768181703321 005 20251116234354.0 010 $a3-540-45685-6 024 7 $a10.1007/3-540-45685-6 035 $a(CKB)1000000000211990 035 $a(SSID)ssj0000327165 035 $a(PQKBManifestationID)11232913 035 $a(PQKBTitleCode)TC0000327165 035 $a(PQKBWorkID)10298634 035 $a(PQKB)11784073 035 $a(DE-He213)978-3-540-45685-8 035 $a(MiAaPQ)EBC3071645 035 $a(PPN)155204688 035 $a(BIP)13638678 035 $a(BIP)7875798 035 $a(EXLCZ)991000000000211990 100 $a20121227d2002 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTheorem Proving in Higher Order Logics $e15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings /$fedited by Victor A. Carreno, Cesar A. Munoz, Sofiene Tahar 205 $a1st ed. 2002. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2002. 215 $a1 online resource (X, 347 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2410 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-540-44039-9 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- Formal Methods at NASA Langley -- Higher Order Unification 30 Years Later -- Regular Papers -- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction -- Efficient Reasoning about Executable Specifications in Coq -- Verified Bytecode Model Checkers -- The 5 Colour Theorem in Isabelle/Isar -- Type-Theoretic Functional Semantics -- A Proposal for a Formal OCL Semantics in Isabelle/HOL -- Explicit Universes for the Calculus of Constructions -- Formalised Cut Admissibility for Display Logic -- Formalizing the Trading Theorem for the Classification of Surfaces -- Free-Style Theorem Proving -- A Comparison of Two Proof Critics: Power vs. Robustness -- Two-Level Meta-reasoning in Coq -- PuzzleTool: An Example of Programming Computation and Deduction -- A Formal Approach to Probabilistic Termination -- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm -- Quotient Types: A Modular Approach -- Sequent Schema for Derived Rules -- Algebraic Structures and Dependent Records -- Proving the Equivalence of Microstep and Macrostep Semantics -- Weakest Precondition for General Recursive Programs Formalized in Coq. 330 $aThis book constitutes the refereed proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, held in Hampton, VA, USA in August 2002.The 20 revised full papers presented together with 2 invited contributions were carefully reviewed and selected from 34 submissions. All current issues in HOL theorem proving and formal verification of software and hardware systems are addressed. Among the HOL theorem proving systems evaluated are Isabelle/HOL, Isabelle/Isar, and Coq. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v2410 606 $aComputer architecture 606 $aComputers 606 $aSoftware engineering 606 $aLogic design 606 $aComputer System Implementation$3https://scigraph.springernature.com/ontologies/product-market-codes/I13057 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050 615 0$aComputer architecture. 615 0$aComputers. 615 0$aSoftware engineering. 615 0$aLogic design. 615 14$aComputer System Implementation. 615 24$aTheory of Computation. 615 24$aSoftware Engineering. 615 24$aLogic Design. 676 $a004/.01/5113 702 $aCarreno$b Victor A$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aMun?oz$b Ce?sar A.$f1968-$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aTahar$b Sofiene$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTPHOLs 2002 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910768181703321 996 $aTheorem Proving in Higher Order Logics$9772309 997 $aUNINA