Theorem Proving in Higher Order Logics  20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings /  [electronic resource] : 
edited by Klaus Schneider, Jens Brandt. 
 - 1st ed. 2007. 
 - VIII, 404 p.  online resource. 
 - Theoretical Computer Science and General Issues,  4732  2512-2029 ; .
 - Theoretical Computer Science and General Issues,  4732 .
<br/><br/>On 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. 
<br/><br/><label>ISBN: </label>9783540745914 
<br/><br/><label>Standard No.: </label>10.1007/978-3-540-74591-4  doi 
<br/><br/><label>Subjects--Topical Terms: </label><br/>Computer science.<br/>Machine theory.<br/>Software engineering.<br/>Artificial intelligence.<br/>Logic design.<br/>Theory of Computation.<br/>Formal Languages and Automata Theory.<br/>Computer Science Logic and Foundations of Programming.<br/>Software Engineering.<br/>Artificial Intelligence.<br/>Logic Design.
<br/><br/><label>LC Class. No.: </label>QA75.5-76.95 
<br/><br/><label>Dewey Class. No.: </label>004.0151