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

Similar Items