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

@InProceedings{TPHOLs2000:BaBe,
   author = {A. Balaa and Y. Bertot},
   title = {Fix-Point Equations for Well-Founded Recursion in Type Theory},
   pages = {1--16},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Barr,
   author = {B. Barras},
   title = {Programming and Computing in {HOL}},
   pages = {17--37},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:BeNi,
   author = {S. Berghofer and T. Nipkow},
   title = {Proof Terms for Simply Typed Higher Order Logic},
   pages = {38--52},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:BhGO,
   author = {K. Bhargavan and C. A. Gunter and D. Obradovic},
   title = {Routing Information Protocol in {HOL}/{SPIN}},
   pages = {53--72},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Capr,
   author = {V. Capretta},
   title = {Recursive Families of Inductive Types},
   pages = {73--89},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:CaMu,
   author = {V. Carre{\~{n}}o and C. Mu{\~{n}}oz},
   title = {Aircraft Trajectory Modeling and Alerting Algorithm Verification},
   pages = {90--105},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:CoBr,
   author = {B. Colwell and B. Brennan},
   title = {{Intel}'s Formal Verification Experience on the {Willamette}
            Development},
   pages = {106--107},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Denn,
   author = {E. Denney},
   title = {A Prototype Proof Translator from {HOL} to {Coq}},
   pages = {108--125},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Dubo,
   author = {C. Dubois},
   title = {Proving {ML} Type Soundness Within {Coq}},
   pages = {126--144},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Fleu,
   author = {J. D. Fleuriot},
   title = {On the Mechanization of Real Analysis in {Isabelle}/{HOL}},
   pages = {145--161},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:GeWZ,
   author = {H. Geuvers and F. Wiedijk and J. Zwanenburg},
   title = {Equational Reasoning via Partial Reflection},
   pages = {162--178},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Gord,
   author = {M. J. C. Gordon},
   title = {Reachability Programming in {HOL98} Using {BDDs}},
   pages = {179--196},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Gott,
   author = {H. Gottliebsen},
   title = {Transcendental Functions and Continuity Checking in {PVS}},
   pages = {197--214},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Grun,
   author = {J. Grundy},
   title = {Verified Optimizations for the {Intel} {IA-64} Architecture},
   pages = {215--232},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Harr,
   author = {J. Harrison},
   title = {Formal Verification of {IA-64} Division Algorithms},
   pages = {233--251},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:HiNo,
   author = {J. Hickey and A. Nogin},
   title = {Fast Tactic-Based Theorem Proving},
   pages = {252--267},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:HoTa,
   author = {M. Hofmann and F. Tang},
   title = {Implementing a Program Logic of Objects in a Higher-Order Logic
            Theorem Prover},
   pages = {268--282},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Holm,
   author = {M. R. Holmes},
   title = {A Strong and Mechanizable Grand Logic},
   pages = {283--300},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:HuJa,
   author = {M. Huisman and B. Jacobs},
   title = {Inheritance in Higher Order Logic: Modeling and Reasoning},
   pages = {301--319},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Jack,
   author = {P. B. Jackson},
   title = {Total-Correctness Refinement for Sequential Reactive Systems},
   pages = {320--337},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:KaAa,
   author = {R. Kaivola and M. D. Aagaard},
   title = {Divider Circuit Verification with Model Checking and Theorem
            Proving},
   pages = {338--355},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:KeNT,
   author = {M. Kerb{\oe}uf and D. Nowak and J.-P. Talpin},
   title = {Specification and Verification of a Steam-Boiler with
            {Signal-Coq}},
   pages = {356--371},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:LavW,
   author = {L. Laibinis and J. von Wright},
   title = {Functional Procedures in Higher-Order Logic},
   pages = {372--387},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:LeTh,
   author = {P. Letouzey and L. Th\'{e}ry},
   title = {Formalizing {St{\aa}lmarck}'s Algorithm in {Coq}},
   pages = {388--405},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:LuWo,
   author = {C. L\"{u}th and B. Wolff},
   title = {{TAS} --- A Generic Window Inference System},
   pages = {406--423},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Merz,
   author = {S. Merz},
   title = {Weak Alternating Automata in {Isabelle}/{HOL}},
   pages = {424--441},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Miln,
   author = {R. Milner},
   title = {Graphical Theories of Interactive Systems:
            Can a Proof Assistant Help?},
   pages = {442},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:MoLe,
   author = {A. Mokkedem and T. Leonard},
   title = {Formal Verification of the {Alpha 21364} Network Protocol},
   pages = {443--461},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Poll,
   author = {R. Pollack},
   title = {Dependently Typed Records for Representing Mathematical Structure},
   pages = {462--479},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:ReHe,
   author = {B. Reus and T. Hein},
   title = {Towards a Machine-Checked {Java} Specification Book},
   pages = {480--497},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Slin,
   author = {K. Slind},
   title = {Another Look at Nested Recursion},
   pages = {498--518},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:WoFi,
   author = {L. Wos and B. Fitelson},
   title = {Automating the Search for Answers to Open Questions},
   pages = {519--525},
   crossref = {TPHOLs2000}}

@InProceedings{TPHOLs2000:Wos,
   author = {L. Wos},
   title = {Appendix: Conjectures Concerning Proof, Design, and Verification},
   pages = {526--533},
   crossref = {TPHOLs2000}}

@Proceedings{TPHOLs2000,
   title = {Proceedings of the 13th International Conference on
            Theorem Proving in Higher Order Logics (TPHOLs 2000)},
   booktitle = {Proceedings of the 13th International Conference on
                Theorem Proving in Higher Order Logics (TPHOLs 2000)},
   year = {2000},
   series = {Lecture Notes in Computer Science},
   volume = {1869},
   editor = {M. Aagaard and J. Harrison},
   publisher = {Springer-Verlag},
   address = {Portland, Oregon, USA},
   month = {August}}