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

49,99 €

inkl. gesetzl. MwSt., Versandkostenfrei

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

28.08.2007

Abbildungen

VIII, 404 p.

Herausgeber

Klaus Schneider + weitere

Verlag

Springer Berlin

Seitenzahl

404

Maße (B/H)

15,5/23,5 cm

Gewicht

628 g

Auflage

1 Auflage 2007

Sprache

Englisch

ISBN

978-3-540-74590-7

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

28.08.2007

Abbildungen

VIII, 404 p.

Herausgeber

Verlag

Springer Berlin

Seitenzahl

404

Maße (B/H)

15,5/23,5 cm

Gewicht

628 g

Auflage

1 Auflage 2007

Sprache

Englisch

ISBN

978-3-540-74590-7

Herstelleradresse

Springer Nature Customer Service Center GmbH
Europaplatz 3
69115 Heidelberg
DE
ProductSafety@springernature.com

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)
  • 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.