InhaltsangabeInvited Talks.- JavaCard Program Verification.- View from the Fringe of the Fringe.- Using Decision Procedures with a Higher-Order Logic.- Regular Contributions.- Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS.- An Irrational Construction of ? from ?.- HELM and the Semantic Math-Web.- Calculational Reasoning Revisited An Isabelle/Isar Experience.- Mechanical Proofs about a Non-repudiation Protocol.- Proving Hybrid Protocols Correct.- Nested General Recursion and Partiality in Type Theory.- A Higher-Order Calculus for Categories.- Certifying the Fast Fourier Transform with Coq.- A Generic Library for Floating-Point Numbers and Its Application to Exact Computing.- Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain.- Abstraction and Refinement in Higher Order Logic.- A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL.- Representing Hierarchical Automata in Interactive Theorem Provers.- Refinement Calculus for Logic Programming in Isabelle/HOL.- Predicate Subtyping with Predicate Sets.- A Structural Embedding of Ocsid in PVS.- A Certified Polynomial-Based Decision Procedure for Propositional Logic.- Finite Set Theory in ACL2.- The HOL/NuPRL Proof Translator.- Formalizing Convex Hull Algorithms.- Experiments with Finite Tree Automata in Coq.- Mizar Light for HOL Light.