Interactive Theorem Proving: First International Conference, Itp 2010, Edinburgh, Uk, July 11-14, 2010, Proceedings

by Kaufmann, Matt; Paulson, Lawrence C.

• ISBN13: 9783642140518
• ISBN10: 3642140513
• Format: Paperback
• Copyright: 2010-07-22
• Publisher: Springer-Verlag New York Inc

Summary

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.

Table of Contents

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