LEADER 05258nam 22007335 450 001 9910143491503321 005 20200629194036.0 010 $a3-540-49801-X 024 7 $a10.1007/BFb0055125 035 $a(CKB)1000000000210979 035 $a(SSID)ssj0000327169 035 $a(PQKBManifestationID)11213082 035 $a(PQKBTitleCode)TC0000327169 035 $a(PQKBWorkID)10316432 035 $a(PQKB)11531550 035 $a(DE-He213)978-3-540-49801-8 035 $a(PPN)155178792 035 $a(EXLCZ)991000000000210979 100 $a20121227d1998 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTheorem Proving in Higher Order Logics$b[electronic resource] $e11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings /$fedited by Jim Grundy, Malcolm Newey 205 $a1st ed. 1998. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1998. 215 $a1 online resource (IX, 496 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1479 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-64987-5 327 $aVerified lexical analysis -- Extending window inference -- Program abstraction in a higher-order logic framework -- The village telephone system: A case study in formal software engineering -- Generating embeddings from denotational descriptions -- An interface between CLAM and HOL -- Classical propositional decidability via Nuprl proof extraction -- A comparison of PVS and Isabelle/HOL -- Adding external decision procedures to HOL90 securely -- Formalizing basic first order model theory -- Formalizing Dijkstra -- Mechanical verification of total correctness through diversion verification conditions -- A type annotation scheme for Nuprl -- Verifying a garbage collection algorithm -- Hot: A concurrent automated theorem prover based on higher-order tableaux -- Free variables and subexpressions in higher-order meta logic -- An LPO-based termination ordering for higher-order terms without ?-abstraction -- Proving isomorphism of first-order logic proof systems in HOL -- Exploiting parallelism in interactive theorem provers -- I/O automata and beyond: Temporal logic and abstraction in Isabelle -- Object-oriented verification based on record subtyping in Higher-Order Logic -- On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system -- Co-inductive axiomatization of a synchronous language -- Formal specification and theorem proving breakthroughs in geometric modeling -- A tool for data refinement -- Mechanizing relevant logics with HOL -- Case studies in meta-level theorem proving -- Formalization of graph search algorithms and its applications. 330 $aThis book constitutes the refereed proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '98, held in Canberra, Australia, in September/October 1998. The 26 revised full papers presented were carefully reviewed and selected from a total of 52 submissions. Also included are two invited papers. The papers address all current aspects of theorem proving in higher order logics and formal verification and program analysis. Besides the HOL system, the theorem provers Coq, Isabelle, LAMBDA, LEGO, NuPrl, and PVS are discussed. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1479 606 $aComputer logic 606 $aArtificial intelligence 606 $aSoftware engineering 606 $aMathematical logic 606 $aLogic design 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 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 logic. 615 0$aArtificial intelligence. 615 0$aSoftware engineering. 615 0$aMathematical logic. 615 0$aLogic design. 615 14$aLogics and Meanings of Programs. 615 24$aArtificial Intelligence. 615 24$aSoftware Engineering/Programming and Operating Systems. 615 24$aMathematical Logic and Formal Languages. 615 24$aSoftware Engineering. 615 24$aLogic Design. 676 $a004/.01/5113 702 $aGrundy$b Jim$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aNewey$b Malcolm$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTPHOLs '98 906 $aBOOK 912 $a9910143491503321 996 $aTheorem Proving in Higher Order Logics$9772309 997 $aUNINA