ITP 2010 Accepted Papers

Importing HOL-Light into Coq
Separation logic adapted for proofs by rewriting
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
A Mechanically Verified AIG-to-BDD Conversion Algorithm
(Nominal) Unification by Recursive Descent with Triangular Substitutions
Formal study of plane Delaunay triangulation
Fast LCF-Style Proof Reconstruction for Z3
A Mechanized Translation from Higher-Order Logic to Set Theory
Programming language techniques for cryptographic proofs
Equations: a dependent pattern-matching compiler
Proof Pearl: A New Foundation for Nominal Isabelle
An Efficient Coq Tactic for Deciding Kleene Algebras
Coverset Induction with Partiality and Subsorts: a Powerlist Case Study
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
The Optimal Fixed Point Combinator
Introducting machine integers and arrays to type theory and its application to SAT verification
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem
Proof Pearl: A formal proof of Duato's condition for deadlock-free adaptive networks
A Framework for Formal Verification of Compiler Optimizations
Case-Analysis for Rippling and Inductive Proof
The Isabelle Collections Framework
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
Automated Machine-Checked Hybrid System Safety Proofs
A tactic language for declarative proofs
Proof Pearl: A Certified Denotational Abstract Interpreter
Using a First Order Logic to Verify That Some Set of Reals Has No Lebesgue Measure
Inductive Consequences in the Calculus of Constructions
Interactive Termination Proofs using Termination Cores
Validating QBF Invalidity in HOL4
On the Formalization of the Lebesgue Integration Theory in HOL
Higher-Order Abstract Syntax in Isabelle/HOL
Developing the algebraic hierarchy with type classes in Coq