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

@InProceedings{TPHOLs98:BeKN,
   author = {M. Benini and S. Kalvala and D. Nowotka},
   title = {Program Abstraction in a Higher-Order Logic Framework},
   pages = {33--48},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:BGGJOZ,
   author = {K. Bhargavan and C. A. Gunter and E. L. Gunter and M. Jackson and
             D. Obradovic and P. Zave},
   title = {{The Village Telephone System}: A Case Study in Formal Software
            Engineering},
   pages = {49--66},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Boul,
   author = {R. J. Boulton},
   title = {Generating Embeddings from Denotational Descriptions},
   pages = {67--86},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:BSBG,
   author = {R. Boulton and K. Slind and A. Bundy and M. Gordon},
   title = {An Interface between {Clam} and {HOL}},
   pages = {87--104},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Cald,
   author = {J. L. Caldwell},
   title = {Classical Propositional Decidability via {Nuprl} Proof
            Extraction},
   pages = {105--122},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:GrHu,
   author = {D. Griffioen and M. Huisman},
   title = {A Comparison of {PVS} and {Isabelle/HOL}},
   pages = {123--142},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Gunt,
   author = {E. L. Gunter},
   title = {Adding External Decision Procedures to {HOL90} Securely},
   pages = {143--152},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Harr1,
   author = {J. Harrison},
   title = {Formalizing Basic First Order Model Theory},
   pages = {153--170},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Harr2,
   author = {J. Harrison},
   title = {Formalizing {Dijkstra}},
   pages = {171--188},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:HoMa,
   author = {P. V. Homeier and D. F. Martin},
   title = {Mechanical Verification of Total Correctness through Diversion
            Verification Conditions},
   pages = {189--206},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Howe,
   author = {D. J. Howe},
   title = {A Type Annotation Scheme for {Nuprl}},
   pages = {207--224},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Jack,
   author = {P. B. Jackson},
   title = {Verifying a Garbage Collection Algorithm},
   pages = {225--244},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Konr,
   author = {K. Konrad},
   title = {{HOT}: A Concurrent Automated Theorem Prover Based on Higher-Order
            Tableaux},
   pages = {245--261},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Lian,
   author = {C. Liang},
   title = {Free Variables and Subexpressions in Higher-Order Meta Logic},
   pages = {263--276},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:LiBa,
   author = {M. Lifantsev and L. Bachmair},
   title = {An {LPO}-based Termination Ordering for Higher-Order Terms without
            $lambda$-abstraction},
   pages = {277--293},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:MivW,
   author = {A. Mikhajlova and J. von Wright},
   title = {Proving Isomorphism of First-Order Logic Proof Systems in {HOL}},
   pages = {295--314},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Mote,
   author = {R. Moten},
   title = {Exploiting Parallelism in Interactive Theorem Provers},
   pages = {315--330},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Mull,
   author = {O. M\"{u}ller},
   title = {{I/O} Automata and Beyond: Temporal Logic and Abstraction in
            {Isabelle}},
   pages = {331--348},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:NaWe,
   author = {W. Naraschewski and M. Wenzel},
   title = {Object-Oriented Verification Based on Record Subtyping in
            Higher-Order Logic},
   pages = {349--366},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:NaVe,
   author = {N. Narasimhan and R. Vemuri},
   title = {On the Effectiveness of Theorem Proving Guided Discovery of Formal
            Assertions for a Register Allocator in a High-Level Synthesis
            System},
   pages = {367--386},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:Nipk,
   author = {T. Nipkow},
   title = {Verified Lexical Analysis},
   pages = {1--15},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:NoBT,
   author = {D. Nowak and J.-R. Beauvais and J.-P. Talpin},
   title = {Co-inductive Axiomatization of a Synchronous Language},
   pages = {387--399},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:PuDu,
   author = {F. Puitg and J.-F. Dufourd},
   title = {Formal Specification and Theorem Proving Breakthroughs in
            Geometric Modeling},
   pages = {401--422},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:RuvW,
   author = {R. Ruk\v{s}\.{e}nas and J. von Wright},
   title = {A Tool for Data Refinement},
   pages = {423--441},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:SaAs,
   author = {H. Sawamura and D. Asanuma},
   title = {Mechanizing Relevant Logics with {HOL}},
   pages = {443--460},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:vHPPR,
   author = {F. W. von Henke and S. Pfab and H. Pfeifer and H. Rue{\ss}},
   title = {Case Studies in Meta-Level Theorem Proving},
   pages = {461--478},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:vonW,
   author = {J. von Wright},
   title = {Extending Window Inference},
   pages = {17--32},
   crossref = {TPHOLs98}}

@InProceedings{TPHOLs98:YTHNT,
   author = {M. Yamamoto and K. Takahashi and M. Hagiya and S. Nishizaki and
             T. Tamai},
   title = {Formalization of Graph Search Algorithms and Its Applications},
   pages = {479--496},
   crossref = {TPHOLs98}}

@Proceedings{TPHOLs98,
   title = {Proceedings of the 11th International Conference on
            Theorem Proving in Higher Order Logics (TPHOLs'98)},
   booktitle = {Proceedings of the 11th International Conference on
                Theorem Proving in Higher Order Logics (TPHOLs'98)},
   year = {1998},
   series = {Lecture Notes in Computer Science},
   volume = {1479},
   editor = {J. Grundy and M. Newey},
   publisher = {Springer},
   address = {Canberra, Australia},
   month = {September/October}}