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

Constance L. Heitmeyer (auth.), Klaus Schneider, Jens Brandt (eds.)3540745904, 9783540745907

This book constitutes the refereed proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, held in Kaiserslautern, Germany, in September 2007.

The 21 revised full papers presented together with 5 proof pearls (concise and elegant presentations of interesting examples) and the abstracts of 3 invited papers were carefully reviewed and selected from 52 submissions. Among the topics of this volume are formal semantics of specification, modelling, 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.

---

Table of contents :
Front Matter….Pages –
On the Utility of Formal Methods in the Development and Certification of Software….Pages 1-2
Formal Techniques in Software Engineering: Correct Software and Safe Systems….Pages 3-4
Separation Logic for Small-Step cminor ….Pages 5-21
Formalising Java’s Data Race Free Guarantee….Pages 22-37
Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL….Pages 38-53
Formalising Generalised Substitutions….Pages 54-69
Extracting Purely Functional Contents from Logical Inductive Types….Pages 70-85
A Modular Formalisation of Finite Group Theory….Pages 86-101
Verifying Nonlinear Real Formulas Via Sums of Squares….Pages 102-118
Verification of Expectation Properties for Discrete Random Variables in HOL….Pages 119-134
A Formally Verified Prover for the $mathcal{ALC,}$ Description Logic….Pages 135-150
Proof Pearl: The Termination Analysis of Terminator ….Pages 151-156
Improving the Usability of HOL Through Controlled Automation Tactics….Pages 157-172
Verified Decision Procedures on Context-Free Grammars….Pages 173-188
Using XCAP to Certify Realistic Systems Code: Machine Context Management….Pages 189-206
Proof Pearl: De Bruijn Terms Really Do Work….Pages 207-222
Proof Pearl: Looping Around the Orbit….Pages 223-231
Source-Level Proof Reconstruction for Interactive Theorem Proving….Pages 232-245
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF….Pages 246-261
Automatically Translating Type and Function Definitions from HOL to ACL2….Pages 262-277
Operational Reasoning for Concurrent Caml Programs and Weak Memory Models….Pages 278-293
Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0 ….Pages 294-301
A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols….Pages 302-318
Primality Proving with Elliptic Curves….Pages 319-333
HOL2P – A System of Classical Higher Order Logic with Second Order Polymorphism….Pages 334-351
Building Formal Method Tools in the Isabelle/Isar Framework….Pages 352-367
Simple Types in Type Theory: Deep and Shallow Encodings….Pages 368-382
Mizar’s Soft Type System….Pages 383-399
Back Matter….Pages –