% 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{TPHOLs2001:ADGKMO,
   author = {A. Adams and M. Dunstan and H. Gottliebsen and T. Kelsey and
             U. Martin and S. Owre},
   title = {Computer Algebra Meets Automated Theorem Proving: 
            Integrating {Maple} and {PVS}},
   pages = {27--42},
   crossref = {TPHOLs2001}}

% Use \usepackage{bbold} in LaTeX2e to obtain the \mathbb macro.
@InProceedings{TPHOLs2001:Arth,
   author = {R. D. Arthan},
   title = {An Irrational Construction of $\mathbb{R}$ from $\mathbb{Z}$},
   pages = {43--58},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:APSS,
   author = {A. Asperti and L. Padovani and {Sacerdoti Coen}, C. and
             I. Schena},
   title = {{HELM} and the {Semantic Math-Web}},
   pages = {59--74},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:BaWe,
   author = {G. Bauer and M. Wenzel},
   title = {Calculational Reasoning Revisited:
            An {Isabelle}/{Isar} Experience},
   pages = {75--90},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:BePa,
   author = {G. Bella and L. C. Paulson},
   title = {Mechanical Proofs about a Non-repudiation Protocol},
   pages = {91--104},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:BKvRL,
   author = {M. Bickford and C. Kreitz and R. van Renesse and X. Liu},
   title = {Proving Hybrid Protocols Correct},
   pages = {105--120},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:BoCa,
   author = {A. Bove and V. Capretta},
   title = {Nested General Recursion and Partiality in Type Theory},
   pages = {121--135},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:CaWi,
   author = {M. C\'{a}ccamo and G. Winskel},
   title = {A Higher-Order Calculus for Categories},
   pages = {136--153},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:Capr,
   author = {V. Capretta},
   title = {Certifying the {Fast Fourier Transform} with {Coq}},
   pages = {154--168},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:DaRT,
   author = {M. Daumas and L. Rideau and L. Th\'{e}ry},
   title = {A Generic Library for Floating-Point Numbers and its Application
            to Exact Computing},
   pages = {169--184},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:DeSm,
   author = {L. A. Dennis and A. Smaill},
   title = {Ordinal Arithmetic: A Case Study for Rippling in a Higher Order
            Domain},
   pages = {185--200},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:FaMC,
   author = {M. Fairtlough and M. Mendler and X. Cheng},
   title = {Abstraction and Refinement in Higher Order Logic},
   pages = {201--216},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:Gay,
   author = {S. J. Gay},
   title = {A Framework for the Formalisation of {Pi Calculus} Type Systems in
            {Isabelle/HOL}},
   pages = {217--232},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:HeKa,
   author = {S. Helke and F. Kamm\"{u}ller},
   title = {Representing Hierarchical Automata in Interactive Theorem Provers},
   pages = {233--248},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:HeHS,
   author = {D. Hemer and I. Hayes and P. Strooper},
   title = {Refinement Calculus for Logic Programming in {Isabelle/HOL}},
   pages = {249--264},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:Hurd,
   author = {J. Hurd},
   title = {Predicate Subtyping with Predicate Sets},
   pages = {265--280},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:Jaco,
   author = {B. Jacobs},
   title = {{JavaCard} Program Verification},
   pages = {1--3},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:John,
   author = {S. D. Johnson},
   title = {View from the Fringe of the Fringe},
   pages = {4},
   crossref = {TPHOLs2001},
   note = {The full paper for this abstract appears in the proceedings of
           \emph{CHARME 2001}, volume 2144 of
           \emph{Lecture Notes in Computer Science}, pages 1--12,
           Springer-Verlag, 2001.}}
%
% The full paper of Johnson's invited talk appears in the CHARME proceedings:
%
@InProceedings{CHARME2001:John,
   author = {S. D. Johnson},
   title = {View from the Fringe of the Fringe (Extended Summary)},
   booktitle = {Proceedings of the 11th {IFIP} {WG 10.5} Advanced Research
                Working Conference on Correct Hardware Design and Verification
                Methods (CHARME 2001)},
   year = {2001},
   series = {Lecture Notes in Computer Science},
   volume = {2144},
   editor = {T. Margaria and T. Melham},
   pages = "1--12",
   publisher = {Springer-Verlag},
   address = {Livingston, Scotland, UK},
   month = {September}}

@InProceedings{TPHOLs2001:Kell,
   author = {P. Kellom\"{a}ki},
   title = {A Structural Embedding of {Ocsid} in {PVS}},
   pages = {281--296},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:MePA,
   author = {I. Medina-Bulo and F. Palomo-Lozano and J. A. Alonso-Jim\'{e}nez},
   title = {A Certified Polynomial-Based Decision Procedure for Propositional
            Logic},
   pages = {297--312},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:Moor,
   author = {J S. Moore},
   title = {Finite Set Theory in {ACL2}},
   pages = {313--328},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:NaSM,
   author = {P. Naumov and M.-O. Stehr and J. Meseguer},
   title = {The {HOL}/{NuPRL} Proof Translator:
            A Practical Approach to Formal Interoperability},
   pages = {329--345},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:PiBe,
   author = {D. Pichardie and Y. Bertot},
   title = {Formalizing Convex Hull Algorithms},
   pages = {346--361},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:RiGo,
   author = {X. Rival and J. Goubault-Larrecq},
   title = {Experiments with Finite Tree Automata in {Coq}},
   pages = {362--377},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:Shan,
   author = {N. Shankar},
   title = {Using Decision Procedures with a Higher-Order Logic},
   pages = {5--26},
   crossref = {TPHOLs2001}}

@InProceedings{TPHOLs2001:Wied,
   author = {F. Wiedijk},
   title = {{Mizar Light} for {HOL Light}},
   pages = {378--393},
   crossref = {TPHOLs2001}}

@Proceedings{TPHOLs2001,
   title = {Proceedings of the 14th International Conference on
            Theorem Proving in Higher Order Logics (TPHOLs 2001)},
   booktitle = {Proceedings of the 14th International Conference on
                Theorem Proving in Higher Order Logics (TPHOLs 2001)},
   year = {2001},
   series = {Lecture Notes in Computer Science},
   volume = {2152},
   editor = {R. J. Boulton and P. B. Jackson},
   publisher = {Springer-Verlag},
   address = {Edinburgh, Scotland, UK},
   month = {September}}