000  04709nam a22006375i 4500  

001  9783540301424  
003  DEHe213  
005  20170515111603.0  
007  cr nn 008mamaa  
008  121227s2004 gw  s  0eng d  
020 
_a9783540301424 _99783540301424 

024  7 
_a10.1007/b100400 _2doi 

050  4  _aQ334342  
050  4  _aTJ210.2211.495  
072  7 
_aUYQ _2bicssc 

072  7 
_aTJFM1 _2bicssc 

072  7 
_aCOM004000 _2bisacsh 

082  0  4 
_a006.3 _223 
245  1  0 
_aTheorem Proving in Higher Order Logics _h[electronic resource] : _b17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 1417, 2004. Proceedings / _cedited by Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan. 
264  1 
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c2004. 

300 
_aVIII, 340 p. _bonline resource. 

336 
_atext _btxt _2rdacontent 

337 
_acomputer _bc _2rdamedia 

338 
_aonline resource _bcr _2rdacarrier 

347 
_atext file _bPDF _2rda 

490  1 
_aLecture Notes in Computer Science, _x03029743 ; _v3223 

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 CookLevin Theorem  Formalizing the Proof of the Kepler Conjecture  Interfacing Hoare Logic and Type Systems for Foundational ProofCarrying 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 FaultTolerant 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.  
520  _aThis volume constitutes the proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004) held September 14–17, 2004 in Park City, Utah, USA. TPHOLs covers all aspects of theorem proving in higherorder logics as well as related topics in theorem proving and veri?cation. There were 42 papers submitted to TPHOLs 2004 in the full research ca gory, each of which was refereed by at least 3 reviewers selected by the program committee. Of these submissions, 21 were accepted for presentation at the c ference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2004 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings c taining papers about inprogress work was published as a 2004 technical report of the School of Computing at the University of Utah. The organizers are grateful to Al Davis, Thomas Hales, and Ken McMillan for agreeing to give invited talks at TPHOLs 2004. The TPHOLs conference traditionally changes continents each year in order to maximize the chances that researchers from around the world can attend.  
650  0  _aComputer science.  
650  0  _aArchitecture, Computer.  
650  0  _aSoftware engineering.  
650  0  _aComputers.  
650  0  _aComputer logic.  
650  0  _aMathematical logic.  
650  0  _aArtificial intelligence.  
650  1  4  _aComputer Science. 
650  2  4  _aArtificial Intelligence (incl. Robotics). 
650  2  4  _aTheory of Computation. 
650  2  4  _aComputer System Implementation. 
650  2  4  _aMathematical Logic and Formal Languages. 
650  2  4  _aLogics and Meanings of Programs. 
650  2  4  _aSoftware Engineering. 
700  1 
_aSlind, Konrad. _eeditor. 

700  1 
_aBunker, Annette. _eeditor. 

700  1 
_aGopalakrishnan, Ganesh. _eeditor. 

710  2  _aSpringerLink (Online service)  
773  0  _tSpringer eBooks  
776  0  8 
_iPrinted edition: _z9783540230175 
830  0 
_aLecture Notes in Computer Science, _x03029743 ; _v3223 

856  4  0  _uhttp://dx.doi.org/10.1007/b100400 
912  _aZDB2SCS  
912  _aZDB2LNC  
912  _aZDB2BAE  
942 
_2ddc _cEB 

950  _aComputer Science (Springer11645)  
999 
_c16269 _d16269 