000 03744nam a22005415i 4500
001 978-3-540-74591-4
003 DE-He213
005 20160624102110.0
007 cr nn 008mamaa
008 100301s2007 gw | s |||| 0|eng d
020 _a9783540745914
_9978-3-540-74591-4
024 7 _a10.1007/978-3-540-74591-4
_2doi
050 4 _aQA8.9-QA10.3
072 7 _aUYA
_2bicssc
072 7 _aMAT018000
_2bisacsh
072 7 _aCOM051010
_2bisacsh
082 0 4 _a005.131
_223
245 1 0 _aTheorem Proving in Higher Order Logics
_h[electronic resource] :
_b20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007. Proceedings /
_cedited by Klaus Schneider, Jens Brandt.
260 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg,
_c2007.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg,
_c2007.
300 _aVIII, 404 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,
_x0302-9743 ;
_v4732
505 0 _aOn the Utility of Formal Methods in the Development and Certification of Software -- Formal Techniques in Software Engineering: Correct Software and Safe Systems -- Separation Logic for Small-Step cminor -- Formalising Java’s Data Race Free Guarantee -- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL -- Formalising Generalised Substitutions -- Extracting Purely Functional Contents from Logical Inductive Types -- A Modular Formalisation of Finite Group Theory -- Verifying Nonlinear Real Formulas Via Sums of Squares -- Verification of Expectation Properties for Discrete Random Variables in HOL -- A Formally Verified Prover for the Description Logic -- Proof Pearl: The Termination Analysis of Terminator -- Improving the Usability of HOL Through Controlled Automation Tactics -- Verified Decision Procedures on Context-Free Grammars -- Using XCAP to Certify Realistic Systems Code: Machine Context Management -- Proof Pearl: De Bruijn Terms Really Do Work -- Proof Pearl: Looping Around the Orbit -- Source-Level Proof Reconstruction for Interactive Theorem Proving -- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF -- Automatically Translating Type and Function Definitions from HOL to ACL2 -- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models -- Proof Pearl: Wellfounded Induction on the Ordinals Up to ? 0 -- A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols -- Primality Proving with Elliptic Curves -- HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism -- Building Formal Method Tools in the Isabelle/Isar Framework -- Simple Types in Type Theory: Deep and Shallow Encodings -- Mizar’s Soft Type System.
650 0 _aComputer science.
650 0 _aLogic design.
650 0 _aSoftware engineering.
650 0 _aArtificial intelligence.
650 1 4 _aComputer Science.
650 2 4 _aMathematical Logic and Formal Languages.
650 2 4 _aLogics and Meanings of Programs.
650 2 4 _aSoftware Engineering.
650 2 4 _aArtificial Intelligence (incl. Robotics).
650 2 4 _aLogic Design.
700 1 _aSchneider, Klaus.
_eeditor.
700 1 _aBrandt, Jens.
_eeditor.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9783540745907
786 _dSpringer
830 0 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v4732
856 4 0 _uhttp://dx.doi.org/10.1007/978-3-540-74591-4
942 _2EBK7774
_cEBK
999 _c37068
_d37068