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

ISBN-13: 9783642140518 / Angielski / Miękka / 2010 / 495 str.

Matt Kaufmann; Lawrence C. Paulson

Opis

This volume contains the papers presented at ITP 2010: the First International ConferenceonInteractiveTheoremProving. It washeldduring July11-14,2010 in Edinburgh, Scotland as part of the Federated Logic Conference (FLoC, July 9-21, 2010) alongside the other FLoC conferences and workshops. ITP combines the communities of two venerable meetings: the TPHOLs c- ference and the ACL2 workshop. The former conference originated in 1988 as a workshop for users of the HOL proof assistant. The ?rst two meetings were at the University of Cambridge, but afterwards they were held in a variety of venues. By 1992, the workshop acquired the name Higher-Order Logic Theorem Proving and Its Applications. In 1996, it was christened anew as Theorem Pr- ing in Higher-Order Logics, TPHOLs for short, and was henceforth organizedas a conference. Each of these transitions broadened the meeting's scope from the original HOL system to include other proof assistants based on forms of high- order logic, including Coq, Isabelle and PVS. TPHOLs has regularly published research done using ACL2 (the modern version of the well-known Boyer-Moore theorem prover), even though ACL2 implements a unique computational form of ?rst-order logic. The ACL2 community has run its own series of workshops since1999. BymergingTPHOLswith the ACL2workshop,weinclude a broader community of researchers who work with interactive proof tools. With our enlarged community, it was not surprising that ITP attracted a record-breaking 74 submissions, each of which was reviewed by at least three Programme Committee members.

Spis treści

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.