TPHOLs 2001: Supplemental Proceedings

• Cover, Title Page (including abstract and copyright notice)
• Preface, Table of Contents
• Hierarchical Verification of the Implementation of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL
  Amr T. Abdel-Hamid, Sofiène Tahar, John Harrison.
• BDD Representation Judgements in HOL : A Performance Evaluation
  Hasan Amjad
• Toward a Verified Generic Prooftool
  Pieter Audenaert
• Some tools for computer-assisted theorem proving in Martin-Löf type theory
  Marcin Benke
• A Lost Proof
  Christoph Benzmüller, Manfred Kerber
• Executing Higher Order Logic
  Stefan Berghofer, Tobias Nipkow
• Proving Type Soundness of a Simply Typed ML-Like Language with References
  Olivier Boite, Catherine Dubois
• B vs. Coq to prove a Garbage Collector
  L. Burdy
• Towards a Generic Tool for Reasoning about Labeled Transition Systems
  Pierre Castéran, Davy Rouillard
• Transformational reasoning with incomplete information
  O. Celiku, J. von Wright
• A User Model for Avoiding Design Induced Errors in Soft-Key Interactive Systems
  Paul Curzon, Ann Blandford
• Constructing Isabelle Proofs in a Proof Refinement Calculus
  Christophe Depasse
• Representing Component States in Higher-Order Logic
  Sidi O. Ehmety, Lawrence C. Paulson
• Complex quantifier elimination in HOL
  John Harrison
• The implementation of an unusual higher-order logic
  M. Randall Holmes
• Quotient Types
  Peter V. Homeier
• A Proof of the Church-Rosser Theorem for the Lambda Calculus in Higher Order Logic
  Peter V. Homeier
• Verification of the Miller-Rabin Probabilistic Primality Test
  Joe Hurd
• Formal Verification of a Theory of IEEE Rounding
  Christian Jacobi
• A PVS Theory of Symbolic Transition Systems
  Savi Maharaj
• A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle
  A. Momigliano, S. J. Ambler, R. L. Crole
• Certification of Matrix Multiplication Algorithms
  Francisco Palomo-Lozano, Inmaculada Medina-Bulo, José A. Alonso-Jiménez
• Quotients in the CCI
  Loïc Pottier
• Proof for Optimization: Programming Logic Support for Java JIT Compilers
  Claire L. Quigley
• An Inductive Approach to Formalizing Notions of Number Theory Proofs}
  Thomas Marthedal Rasmussen
• Verifying that Invariants are Context-Inductive
  Vlad Rusu}
• Tactics in modern proof-assistants: the bad habit of overkilling
  Claudio Sacerdoti Coen
• Mechanizing in Higher-Order Logic Proofs of Correctness and Completeness for a Set of RTL Transformations
  Elena Teica, Ranga Vemuri
• Proving Existential Theorems when Importing Results from MDG to HOL
  Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford
• Translating HOL to Specifications for the Model Checker SMV
  Dan Zhou, Paul E. Black
• Author Index