• Produktbild: Theorem Proving in Higher Order Logics
  • Produktbild: Theorem Proving in Higher Order Logics

Theorem Proving in Higher Order Logics 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009, Proceedings

Fr. 73.90

inkl. gesetzl. MwSt., Versandkostenfrei


Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

04.08.2009

Herausgeber

Stefan Berghofer + weitere

Verlag

Springer Berlin

Seitenzahl

517

Maße (L/B/H)

23.5/15.5/2.9 cm

Gewicht

797 g

Auflage

2009

Sprache

Englisch

ISBN

978-3-642-03358-2

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

04.08.2009

Herausgeber

Verlag

Springer Berlin

Seitenzahl

517

Maße (L/B/H)

23.5/15.5/2.9 cm

Gewicht

797 g

Auflage

2009

Sprache

Englisch

ISBN

978-3-642-03358-2

Herstelleradresse

Springer-Verlag KG
Sachsenplatz 4-6
1201 Wien
AT

Email: GPSR Kontakt

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
  • Produktbild: Theorem Proving in Higher Order Logics
  • Invited Papers.- Let’s Get Physical: Models and Methods for Real-World Security Protocols.- VCC: A Practical System for Verifying Concurrent C.- Without Loss of Generality.- Invited Tutorials.- HOL Light: An Overview.- A Brief Overview of Mizar.- A Brief Overview of Agda – A Functional Language with Dependent Types.- The Twelf Proof Assistant.- Regular Papers.- Hints in Unification.- Psi-calculi in Isabelle.- Some Domain Theory and Denotational Semantics in Coq.- Turning Inductive into Equational Specifications.- Formalizing the Logic-Automaton Connection.- Extended First-Order Logic.- Formalising Observer Theory for Environment-Sensitive Bisimulation.- Formal Certification of a Resource-Aware Language Implementation.- A Certified Data Race Analysis for a Java-like Language.- Formal Analysis of Optical Waveguides in HOL.- The HOL-Omega Logic.- A Purely Definitional Universal Domain.- Types, Maps and Separation Logic.- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence.- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL.- Packaging Mathematical Structures.- Practical Tactics for Separation Logic.- Verified LISP Implementations on ARM, x86 and PowerPC.- Trace-Based Coinductive Operational Semantics for While.- A Better x86 Memory Model: x86-TSO.- Formal Verification of Exact Computations Using Newton’s Method.- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.- A Hoare Logic for the State Monad.- Certification of Termination Proofs Using CeTA.- A Formalisation of Smallfoot in HOL.- Liveness Reasoning with Isabelle/HOL.- Mind the Gap.