Theorem proving in higher order logics : 21st international conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008 ; proceedings

Annotation This book constitutes the refereed proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008, held in Montreal, Canada, in August 2008. The 17 revised full papers presented together with 1 proof pearl (concise and elegant presentations of interesting examples), 5 tool presentations, and 2 invited papers were carefully reviewed and selected from 40 submissions. The papers cover all aspects of theorem proving in higher order logics as well as related topics in theorem proving and verification such as formal semantics of specification, modeling, and programming languages, specification and verification of hardware and software, formalisation of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers Front Matter....Pages - Twenty Years of Theorem Proving for HOLs Past, Present and Future....Pages 1-5 Will This Be Formal?....Pages 6-11 A Short Presentation of Coq....Pages 12-16 An ACL2 Tutorial....Pages 17-21 A Brief Overview of PVS....Pages 22-27 A Brief Overview of HOL4....Pages 28-32 The Isabelle Framework....Pages 33-38 A Compiled Implementation of Normalization by Evaluation....Pages 39-54 LCF-Style Propositional Simplification with BDDs and SAT Solvers....Pages 55-70 Nominal Inversion Principles....Pages 71-85 Canonical Big Operators....Pages 86-101 A Type of Partial Recursive Functions....Pages 102-117 Formal Reasoning About Causality Analysis....Pages 118-133 Imperative Functional Programming with Isabelle/HOL....Pages 134-149 HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier....Pages 150-166 Secure Microkernels, State Monads and Scalable Refinement....Pages 167-182 Certifying a Termination Criterion Based on Graphs, without Graphs....Pages 183-198 Lightweight Separation....Pages 199-214 Real Number Calculations and Theorem Proving....Pages 215-229 A Formalized Theory for Verifying Stability and Convergence of Automata in PVS....Pages 230-245 Certified Exact Transcendental Real Number Computation in Coq....Pages 246-261 Formalizing Soundness of Contextual Effects....Pages 262-277 First-Class Type Classes....Pages 278-293 Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL....Pages 294-309 Proof Pearl: Revisiting the Mini-rubik in Coq....Pages 310-319 Back Matter....Pages - Otmane Ait Mohamed, Cesar Munoz, Sofiene Tahar (eds.). International Conference Proceedings. Includes Bibliographical References And Index.