LEADER 04465nam 22007935 450 001 996465287103316 005 20230222032210.0 010 $a3-540-74591-2 024 7 $a10.1007/978-3-540-74591-4 035 $a(CKB)1000000000491030 035 $a(SSID)ssj0000320357 035 $a(PQKBManifestationID)11235216 035 $a(PQKBTitleCode)TC0000320357 035 $a(PQKBWorkID)10257688 035 $a(PQKB)10231438 035 $a(DE-He213)978-3-540-74591-4 035 $a(MiAaPQ)EBC3063201 035 $a(MiAaPQ)EBC6707296 035 $a(Au-PeEL)EBL6707296 035 $a(PPN)123164680 035 $a(EXLCZ)991000000000491030 100 $a20100301d2007 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] $e20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings /$fedited by Klaus Schneider, Jens Brandt 205 $a1st ed. 2007. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2007. 215 $a1 online resource (VIII, 404 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4732 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-74590-4 320 $aIncludes bibliographical references and index. 327 $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. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4732 606 $aComputer science 606 $aMachine theory 606 $aSoftware engineering 606 $aArtificial intelligence 606 $aLogic design 606 $aTheory of Computation 606 $aFormal Languages and Automata Theory 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aArtificial Intelligence 606 $aLogic Design 615 0$aComputer science. 615 0$aMachine theory. 615 0$aSoftware engineering. 615 0$aArtificial intelligence. 615 0$aLogic design. 615 14$aTheory of Computation. 615 24$aFormal Languages and Automata Theory. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aArtificial Intelligence. 615 24$aLogic Design. 676 $a005.115 702 $aSchneider$b Klaus$f1967- 702 $aBrandt$b Jens$f1978- 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465287103316 996 $aTheorem Proving in Higher Order Logics$9772309 997 $aUNISA