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

• Corporate Author: SpringerLink (Online service)
• Other Authors: Schneider, Klaus (Editor), Brandt, Jens (Editor)
• Format: Electronic eBook
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007.
• Series: Lecture Notes in Computer Science, 4732
• Subjects: Computer science.; Logic design.; Software engineering.; Computers.; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Theory of Computation.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Software Engineering.; Artificial Intelligence (incl. Robotics).; Logic Design.

Table of Contents:

• 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.