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
Paul Jackson
Last modified: Mon Oct 22 18:32:23 BST 2001