Interactive Theorem Proving: First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings by Matt KaufmannInteractive Theorem Proving: First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings by Matt Kaufmann

Interactive Theorem Proving: First International Conference, ITP 2010 Edinburgh, UK, July 11-14…

byMatt KaufmannEditorLawrence C. Paulson

Paperback | June 30, 2010

Pricing and Purchase Info

$205.95

Earn 1,030 plum® points

Prices and offers may vary in store

Quantity:

In stock online

Ships free on orders over $25

Not available in stores

about

This book constitutes the refereed proceedings of the First International Conference on Interactive Theorem proving, ITP 2010, held in Edinburgh, UK, in July 2010. The 33 revised full papers presented were carefully reviewed and selected from 74 submissions. The papers are organized in topics such as counterexample generation, hybrid system verification, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc.
Title:Interactive Theorem Proving: First International Conference, ITP 2010 Edinburgh, UK, July 11-14…Format:PaperbackDimensions:495 pages, 0.88 × 0.64 × 0.02 inPublished:June 30, 2010Publisher:Springer-Verlag/Sci-Tech/TradeLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:3642140513

ISBN - 13:9783642140518

Look for similar items by category:

Reviews

Table of Contents

Invited Talks.- A Formally Verified OS Kernel. Now What?.- Proof Assistants as Teaching Assistants: A View from the Trenches.- Proof Pearls.- A Certified Denotational Abstract Interpreter.- Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure.- A New Foundation for Nominal Isabelle.- (Nominal) Unification by Recursive Descent with Triangular Substitutions.- A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks.- Regular Papers.- Extending Coq with Imperative Features and Its Application to SAT Verification.- A Tactic Language for Declarative Proofs.- Programming Language Techniques for Cryptographic Proofs.- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder.- Formal Proof of a Wave Equation Resolution Scheme: The Method Error.- An Efficient Coq Tactic for Deciding Kleene Algebras.- Fast LCF-Style Proof Reconstruction for Z3.- The Optimal Fixed Point Combinator.- Formal Study of Plane Delaunay Triangulation.- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison.- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.- Automated Machine-Checked Hybrid System Safety Proofs.- Coverset Induction with Partiality and Subsorts: A Powerlist Case Study.- Case-Analysis for Rippling and Inductive Proof.- Importing HOL Light into Coq.- A Mechanized Translation from Higher-Order Logic to Set Theory.- The Isabelle Collections Framework.- Interactive Termination Proofs Using Termination Cores.- A Framework for Formal Verification of Compiler Optimizations.- On the Formalization of the Lebesgue Integration Theory in HOL.- From Total Store Order to Sequential Consistency: A Practical Reduction Theorem.- Equations: A Dependent Pattern-Matching Compiler.- A Mechanically Verified AIG-to-BDD Conversion Algorithm.- Inductive Consequences in the Calculus of Constructions.- Validating QBF Invalidity in HOL4.- Rough Diamonds.- Higher-Order Abstract Syntax in Isabelle/HOL.- Separation Logic Adapted for Proofs by Rewriting.- Developing the Algebraic Hierarchy with Type Classes in Coq.