000 04143nam a22006015i 4500
001 978-3-540-74591-4
003 DE-He213
005 20240730184634.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 _aQA75.5-76.95
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a004.0151
_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.
250 _a1st ed. 2007.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_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 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_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.
_99832
650 0 _aMachine theory.
_9136155
650 0 _aSoftware engineering.
_94138
650 0 _aArtificial intelligence.
_93407
650 0 _aLogic design.
_93686
650 1 4 _aTheory of Computation.
_9136156
650 2 4 _aFormal Languages and Automata Theory.
_9136157
650 2 4 _aComputer Science Logic and Foundations of Programming.
_942203
650 2 4 _aSoftware Engineering.
_94138
650 2 4 _aArtificial Intelligence.
_93407
650 2 4 _aLogic Design.
_93686
700 1 _aSchneider, Klaus.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9136158
700 1 _aBrandt, Jens.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9136159
710 2 _aSpringerLink (Online service)
_9136160
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540745907
776 0 8 _iPrinted edition:
_z9783540843139
830 0 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v4732
_9136161
856 4 0 _uhttps://doi.org/10.1007/978-3-540-74591-4
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c92408
_d92408