000 05788cam a2200793 i 4500
001 ocm57348553
003 OCoLC
005 20250703143131.0
006 m o d
007 cr |||||||||||
008 041210s2004 gw a ob 101 u eng d
040 _aQCL
_beng
_epn
_cQCL
_dOCLCQ
_dN$T
_dYDXCP
_dOCLCQ
_dYNG
_dOCLCQ
_dDKDLA
_dOCLCQ
_dOCLCO
_dOCLCQ
_dGW5XE
_dOCLCF
_dOCLCQ
_dOCLCO
_dOCLCQ
_dAZU
_dOCL
_dOCLCO
_dOCLCQ
_dEBLCP
_dUAB
_dESU
_dVT2
_dOCLCA
_dOCLCQ
_dOCLCA
_dWYU
_dOL$
_dOCLCQ
_dAUD
_dOCLCQ
_dLUN
_dEUX
_dOCLCQ
_dOCLCO
_dOCLCQ
_dINT
_dOCLCO
_dWSU
_dOCLCO
_dOCLCL
_dOCLCO
_dOCLCQ
016 7 _a97200064X
_2DE-101
019 _a62458722
_a144566218
_a729901537
_a768063540
_a1005777757
_a1066605878
_a1081200939
_a1105602973
_a1132296414
_a1171549881
_a1172183936
_a1239211893
_a1374611682
020 _a3540301429
_q(electronic bk.)
020 _a9783540301424
_q(electronic bk.)
020 _z3540230173
020 _z9783540230175
020 _a9788354030140
_q(4)
020 _a8354030148
024 7 _a10.1007/b100400
_2doi
029 1 _aAU@
_b000051345755
029 1 _aNZ1
_b14990912
029 1 _aNZ1
_b15296648
029 1 _aDKDLA
_b820120-katalog:999912299205765
029 1 _aAU@
_b000078468973
035 _a(OCoLC)57348553
_z(OCoLC)62458722
_z(OCoLC)144566218
_z(OCoLC)729901537
_z(OCoLC)768063540
_z(OCoLC)1005777757
_z(OCoLC)1066605878
_z(OCoLC)1081200939
_z(OCoLC)1105602973
_z(OCoLC)1132296414
_z(OCoLC)1171549881
_z(OCoLC)1172183936
_z(OCoLC)1239211893
_z(OCoLC)1374611682
050 4 _aQA76.9.A96
_bT655 2004eb
072 7 _aCOM
_x025000
_2bisacsh
072 7 _aQA
_2lcco
082 0 4 _a006.333
_222
049 _aMAIN
111 2 _aTPHOLs
_n(17th :
_d2004 :
_cPark City, Utah)
_918618
245 1 0 _aTheorem proving in higher order logics :
_b17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004 : proceedings /
_ceditors, Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan.
246 3 0 _aTPHOLs 2004
260 _aBerlin :
_bSpringer,
_c2004.
300 _a1 online resource (viii, 336 pages) :
_billustrations
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_2rdaft
_0http://rdaregistry.info/termList/fileType/1002
490 1 _aLecture notes in computer science ;
_v3223
500 _aTitle from title screen (viewed December 10, 2004).
500 _aPrint version originally published in 2004.
504 _aIncludes bibliographical references and index.
520 _aThis book constitutes the refereed proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2004, held in Park City, Utah, USA, in September 2004. The 21 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 42 submissions. Among the topics addressed are theorem proving, verification, inductive types, automated deduction, mechanized proofs, mathematical logic, proof theory, type systems, computability, program verification, ACL, Cop, Isabelle/HOL, recursive functions, integration theory, machine code safety certification, and abstraction.
505 0 _aError Analysis of Digital Filters Using Theorem Proving -- Verifying Uniqueness in a Logical Framework -- A Program Logic for Resource Verification -- Proof Reuse with Extended Inductive Types -- Hierarchical Reflection -- Correct Embedded Computing Futures -- Higher Order Rippling in IsaPlanner -- A Mechanical Proof of the Cook-Levin Theorem -- Formalizing the Proof of the Kepler Conjecture -- Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code -- Extensible Hierarchical Tactic Construction in a Logical Framework -- Theorem Reuse by Proof Term Transformation -- Proving Compatibility Using Refinement -- Java Program Verification via a JVM Deep Embedding in ACL2 -- Reasoning About CBV Functional Programs in Isabelle/HOL -- Proof Pearl: From Concrete to Functional Unparsing -- A Decision Procedure for Geometry in Coq -- Recursive Function Definition for Types with Binders -- Abstractions for Fault-Tolerant Distributed System Verification -- Formalizing Integration Theory with an Application to Probabilistic Algorithms -- Formalizing Java Dynamic Loading in HOL -- Certifying Machine Code Safety: Shallow Versus Deep Embedding -- Term Algebras with Length Function and Bounded Quantifier Alternation.
650 0 _aAutomatic theorem proving
_vCongresses.
_914919
650 6 _aThéorèmes
_xDémonstration automatique
_vCongrès.
_914921
650 7 _aCOMPUTERS
_xExpert Systems.
_2bisacsh
_917903
650 7 _aAutomatic theorem proving
_2fast
_914923
655 7 _aproceedings (reports)
_2aat
655 7 _aConference papers and proceedings
_2fast
_96065
655 7 _aConference papers and proceedings.
_2lcgft
_96065
655 7 _aActes de congrès.
_2rvmgf
_9609890
700 1 _aSlind, Konrad.
_918619
700 1 _aBunker, Annette.
_918620
700 1 _aGopalakrishnan, Ganesh.
_918621
710 2 _aLINK (Online service)
_1https://id.oclc.org/worldcat/entity/E39QH7JmqkRqbCq7YPR7CghJc6
758 _ihas work:
_aTheorem proving in higher order logics (Text)
_1https://id.oclc.org/worldcat/entity/E39PCFCmDpRkX6TGPqGdbxVxQq
_4https://id.oclc.org/worldcat/ontology/hasWork
776 0 8 _iPrint version:
_aTPHOLs 2004 (2004 : Park City, Utah).
_tTheorem proving in higher order logics.
_dBerlin ; New York : Springer, 2004
_z3540230173
_w(DLC) 2004111288
_w(OCoLC)56492378
830 0 _aLecture notes in computer science ;
_v3223.
856 4 0 _uhttps://link.springer.com/10.1007/b100400
938 _aProQuest Ebook Central
_bEBLB
_nEBL3087845
938 _aEBSCOhost
_bEBSC
_n144507
938 _aYBP Library Services
_bYANK
_n2367960
936 _aBATCHLOAD
994 _a92
_bATIST
999 _c635768
_d635768