Vor Ort
Merkzettel Warenkorb
Produktbild: Theorem Proving in Higher Order Logics
Band 4732

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

Aus der Reihe Lecture Notes in Computer Science

51,99 €

inkl. gesetzl. MwSt., Versandkostenfrei

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

28.08.2007

Herausgeber

Klaus Schneider + weitere

Verlag

Springer Berlin

Seitenzahl

404

Maße (L/B/H)

23,9/15,7/2,7 cm

Gewicht

628 g

Auflage

2007

Sprache

Englisch

ISBN

978-3-540-74590-7

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

28.08.2007

Herausgeber

Verlag

Springer Berlin

Seitenzahl

404

Maße (L/B/H)

23,9/15,7/2,7 cm

Gewicht

628 g

Auflage

2007

Sprache

Englisch

ISBN

978-3-540-74590-7

Herstelleradresse

Springer-Verlag GmbH
Heidelberger Platz 3
14197 Berlin
Deutschland
Email: sdc-bookservice@springer.com
Url: www.springer.com
Telephone: +49 6221 3454301
Fax: +49 30 8214091

Kundinnen und Kunden meinen

0 Bewertungen

Informationen zu Bewertungen

Zur Abgabe einer Bewertung ist eine Anmeldung im Konto notwendig. Die Authentizität der Bewertungen wird von uns nicht überprüft. Wir behalten uns vor, Bewertungstexte, die unseren Richtlinien widersprechen, entsprechend zu kürzen oder zu löschen.

Die Bewertungen sind nach Format, Anzahl Sterne und Datum sortiert.

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kund*innen durch Ihre Meinung

Kundinnen und Kunden meinen

0 Bewertungen filtern
  • Produktbild: Theorem Proving in Higher Order Logics
  • 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.