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

Front Matter....Pages -
A Formally Verified OS Kernel. Now What?....Pages 1-7
Proof Assistants as Teaching Assistants: A View from the Trenches....Pages 8-8
A Certified Denotational Abstract Interpreter....Pages 9-24
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure....Pages 25-34
A New Foundation for Nominal Isabelle....Pages 35-50
(Nominal) Unification by Recursive Descent with Triangular Substitutions....Pages 51-66
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks....Pages 67-82
Extending Coq with Imperative Features and Its Application to SAT Verification....Pages 83-98
A Tactic Language for Declarative Proofs....Pages 99-114
Programming Language Techniques for Cryptographic Proofs....Pages 115-130
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder....Pages 131-146
Formal Proof of a Wave Equation Resolution Scheme: The Method Error....Pages 147-162
An Efficient Coq Tactic for Deciding Kleene Algebras....Pages 163-178
Fast LCF-Style Proof Reconstruction for Z3....Pages 179-194
The Optimal Fixed Point Combinator....Pages 195-210
Formal Study of Plane Delaunay Triangulation....Pages 211-226
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison....Pages 227-242
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture....Pages 243-258
Automated Machine-Checked Hybrid System Safety Proofs....Pages 259-274
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study....Pages 275-290
Case-Analysis for Rippling and Inductive Proof....Pages 291-306
Importing HOL Light into Coq....Pages 307-322
A Mechanized Translation from Higher-Order Logic to Set Theory....Pages 323-338
The Isabelle Collections Framework....Pages 339-354
Interactive Termination Proofs Using Termination Cores....Pages 355-370
A Framework for Formal Verification of Compiler Optimizations....Pages 371-386
On the Formalization of the Lebesgue Integration Theory in HOL....Pages 387-402
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem....Pages 403-418
Equations: A Dependent Pattern-Matching Compiler....Pages 419-434
A Mechanically Verified AIG-to-BDD Conversion Algorithm....Pages 435-449
Inductive Consequences in the Calculus of Constructions....Pages 450-465
Validating QBF Invalidity in HOL4....Pages 466-480
Higher-Order Abstract Syntax in Isabelle/HOL....Pages 481-484
Separation Logic Adapted for Proofs by Rewriting....Pages 485-489
Developing the Algebraic Hierarchy with Type Classes in Coq....Pages 490-493
Back Matter....Pages -