% Supplemental Proceedings of the 14th International Conference on
% Theorem Proving in Higher Order Logics
%
% The entry for the full proceedings is at the end of the file.

@InProceedings{TPHOLs2001Supp:AbTH,
   author = {A. T. Abdel-Hamid and S. Tahar and J. Harrison},
   title = {Hierarchical Verification of the Implementation of the {IEEE-754}
            Table-Driven Floating-Point Exponential Function using {HOL}},
   pages = {1--16},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Amja,
   author = {H. Amjad},
   title = {{BDD} Representation Judgements in {HOL}:
            A Performance Evaluation},
   pages = {17--26},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Aude,
   author = {P. Audenaert},
   title = {Toward a Verified Generic Prooftool},
   pages = {27--34},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Benk,
   author = {M. Benke},
   title = {Some Tools for Computer-Assisted Theorem Proving in
            {Martin-L\"{o}f} Type Theory},
   pages = {35--39},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:BeKe,
   author = {C. Benzm\"{u}ller and M. Kerber},
   title = {A Lost Proof},
   pages = {40--52},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:BeNi,
   author = {S. Berghofer and T. Nipkow},
   title = {Executing Higher Order Logic},
   pages = {53--68},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:BoDu,
   author = {O. Boite and C. Dubois},
   title = {Proving Type Soundness of a Simply Typed {ML}-Like Language with
            References},
   pages = {69--84},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Burd,
   author = {L. Burdy},
   title = {{B} vs. {Coq} to Prove a Garbage Collector},
   pages = {85--97},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:CaRo,
   author = {P. Cast\'{e}ran and D. Rouillard},
   title = {Towards a Generic Tool for Reasoning about Labeled Transition
            Systems},
   pages = {98--106},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:CevW,
   author = {O. Celiku and J. von Wright},
   title = {Transformational Reasoning with Incomplete Information},
   pages = {107--120},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:CuBl,
   author = {P. Curzon and A. Blandford},
   title = {A User Model for Avoiding Design Induced Errors in Soft-Key
            Interactive Systems},
   pages = {121--136},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Depa,
   author = {C. Depasse},
   title = {Constructing {Isabelle} Proofs in a Proof Refinement Calculus},
   pages = {137--150},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:EhPa,
   author = {S. O. Ehmety and L. C. Paulson},
   title = {Representing Component States in Higher-Order Logic},
   pages = {151--158},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Harr,
   author = {J. Harrison},
   title = {Complex Quantifier Elimination in {HOL}},
   pages = {159--174},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Holm,
   author = {M. R. Holmes},
   title = {The Implementation of an Unusual Higher-Order Logic},
   pages = {175--190},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Home1,
   author = {P. V. Homeier},
   title = {Quotient Types},
   pages = {191--206},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Home2,
   author = {P. V. Homeier},
   title = {A Proof of the {Church-Rosser} Theorem for the Lambda Calculus in
            Higher Order Logic},
   pages = {207--222},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Hurd,
   author = {J. Hurd},
   title = {Verification of the {Miller-Rabin} Probabilistic Primality Test},
   pages = {223--238},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Jaco,
   author = {C. Jacobi},
   title = {Formal Verification of a Theory of {IEEE} Rounding},
   pages = {239--254},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Maha,
   author = {S. Maharaj},
   title = {A {PVS} Theory of Symbolic Transition Systems},
   pages = {255--266},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:MoAC,
   author = {A. Momigliano and S. J. Ambler and R. L. Crole},
   title = {A Comparison of Formalizations of the Meta-Theory of a Language
            with Variable Bindings in {Isabelle}},
   pages = {267--282},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:PaMA,
   author = {F. Palomo-Lozano and I. Medina-Bulo and J. A. Alonso-Jim\'{e}nez},
   title = {Certification of Matrix Multiplication Algorithms:
            {Strassen}'s Algorithm in {ACL2}},
   pages = {283--298},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Pott,
   author = {L. Pottier},
   title = {Quotients in the {CIC}},
   pages = {299--312},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Quig,
   author = {C. L. Quigley},
   title = {Proof for Optimization:
            Programming Logic Support for {Java} {JIT} Compilers},
   pages = {313--327},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Rasm,
   author = {T. M. Rasmussen},
   title = {An Inductive Approach to Formalizing Notions of Number Theory
            Proofs},
   pages = {328--336},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Rusu,
   author = {V. Rusu},
   title = {Verifying that Invariants are Context-Inductive},
   pages = {337--351},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:Sace,
   author = {{Sacerdoti Coen}, C.},
   title = {Tactics in Modern Proof-Assistants: The Bad Habit of Overkilling},
   pages = {352--367},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:TeVe,
   author = {E. Teica and R. Vemuri},
   title = {Mechanizing in Higher-Order Logic Proofs of Correctness and
            Completeness for a Set of {RTL} Transformations},
   pages = {368--383},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:XCTB,
   author = {H. Xiong and P. Curzon and S. Tahar and A. Blandford},
   title = {Proving Existential Theorems when Importing Results from {MDG} to
            {HOL}},
   pages = {384--399},
   crossref = {TPHOLs2001Supp}}

@InProceedings{TPHOLs2001Supp:ZhBl,
   author = {D. Zhou and P. E. Black},
   title = {Translating {HOL} to Specifications for the Model Checker {SMV}},
   pages = {400--415},
   crossref = {TPHOLs2001Supp}}

@Proceedings{TPHOLs2001Supp,
   title = {{TPHOLs 2001}: Supplemental Proceedings},
   booktitle = {{TPHOLs 2001}: Supplemental Proceedings},
   series = {Informatics Report Series},
   number = {EDI-INF-RR-0046},
   year = {2001},
   editor = {R. J. Boulton and P. B. Jackson},
   organization = {Division of Informatics, University of Edinburgh,
                   Edinburgh, Scotland, UK},
   month = {September},
   url = {http://www.informatics.ed.ac.uk/publications/report/0046.html}}