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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Kaufmann, Matt (Επιμελητής έκδοσης), Paulson, Lawrence C. (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2010.
• Σειρά: Lecture Notes in Computer Science, 6172
• Θέματα: Computer science.; Antibodies.; Software engineering.; Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Logics and Meanings of Programs.; Software Engineering.; Mathematical Logic and Formal Languages.; Programming Languages, Compilers, Interpreters.; Artificial Intelligence (incl. Robotics).

Πίνακας περιεχομένων:

• 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.