Cover Image
Read Now

Theorem Proving in Higher Order Logics 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings

Bibliographic Details
Other Authors: Schneider, Klaus (Editor), Brandt, Jens (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 2007, 2007
Edition:1st ed. 2007
Series:Theoretical Computer Science and General Issues
Subjects:
Computer Science Logic And Foundations Of Programming
Software Engineering
Computer Science
Artificial Intelligence
Formal Languages And Automata Theory
Machine Theory
Logic Design
Theory Of Computation
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
LEADER 03199nmm a2200385 u 4500
001 EB000379388
003 EBX01000000000000000232440
005 00000000000000.0
007 cr|||||||||||||||||||||
008 130626 ||| eng
020 |a 9783540745914 
100 1 |a Schneider, Klaus  |e [editor] 
245 0 0 |a Theorem Proving in Higher Order Logics  |h Elektronische Ressource  |b 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings  |c edited by Klaus Schneider, Jens Brandt 
250 |a 1st ed. 2007 
260 |a Berlin, Heidelberg  |b Springer Berlin Heidelberg  |c 2007, 2007 
300 |a VIII, 404 p  |b online resource 
505 0 |a 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 
653 |a Computer Science Logic and Foundations of Programming 
653 |a Software engineering 
653 |a Computer science 
653 |a Artificial Intelligence 
653 |a Software Engineering 
653 |a Formal Languages and Automata Theory 
653 |a Machine theory 
653 |a Artificial intelligence 
653 |a Logic design 
653 |a Logic Design 
653 |a Theory of Computation 
700 1 |a Brandt, Jens  |e [editor] 
041 0 7 |a eng  |2 ISO 639-2 
989 |b Springer  |a Springer eBooks 2005- 
490 0 |a Theoretical Computer Science and General Issues 
028 5 0 |a 10.1007/978-3-540-74591-4 
856 4 0 |u https://doi.org/10.1007/978-3-540-74591-4?nosfx=y  |x Verlag  |3 Volltext 
082 0 |a 004.0151 

Similar Items