Jetzt 20% Rabatt auf alle English Books. Jetzt in über 4 Millionen Büchern stöbern und profitieren!
Willkommen, schön sind Sie da!
Logo Ex Libris

Theorem Proving in Higher Order Logics

  • Kartonierter Einband
  • 404 Seiten
(0) Erste Bewertung abgeben
Alle Bewertungen ansehen
This book contains the refereed proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs... Weiterlesen
126.00 CHF 100.80
Sie sparen CHF 25.20
Exemplar wird für Sie besorgt.
Kein Rückgaberecht!
Bestellung & Lieferung in eine Filiale möglich


This book contains the refereed proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, held in Kaiserslautern, Germany, September 2007. Among the topics of this volume are formal semantics of specification, modeling, and programming languages, specification and verification of hardware and software, formalization of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers.

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.


Titel: Theorem Proving in Higher Order Logics
Untertitel: 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings
EAN: 9783540745907
ISBN: 978-3-540-74590-7
Format: Kartonierter Einband
Herausgeber: Springer, Berlin
Genre: Informatik
Anzahl Seiten: 404
Größe: H235mm x B235mm x T155mm
Jahr: 2007
Untertitel: Englisch
Auflage: 2007

Weitere Produkte aus der Reihe "Theoretical Computer Science and General Issues"