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

@InProceedings{TPHOLs99:AaJS,
   author = {M. D. Aagaard and R. B. Jones and C.-J. H. Seger},
   title = {{Lifted-FL}: A Pragmatic Implementation of Combined Model
            Checking and Theorem Proving},
   pages = {323--340},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:AmCr,
   author = {S. J. Ambler and R. L. Crole},
   title = {Mechanized Operational Semantics via (Co)Induction},
   pages = {221--238},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:BeWe,
   author = {S. Berghofer and M. Wenzel},
   title = {Inductive Datatypes in {HOL} ---
            Lessons Learned in Formal-Logic Engineering},
   pages = {19--36},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Boli,
   author = {D. Bolignano},
   title = {Formal Methods and Security Evaluation},
   pages = {291},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Capr,
   author = {V. Capretta},
   title = {Universal Algebra in Type Theory},
   pages = {131--148},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:CaCo,
   author = {O. Caprotti and A. M. Cohen},
   title = {Connecting Proof Checkers and Computer Algebra Using {OpenMath}},
   pages = {109--112},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:CoJa,
   author = {S. Coupet-Grimal and L. Jakubiec},
   title = {Hardware Verification Using Co-induction in {COQ}},
   pages = {91--108},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:DaJo,
   author = {N. A. Day and J. J. Joyce},
   title = {Symbolic Functional Evaluation},
   pages = {341--358},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:GrMu,
   author = {B. Grobauer and O. M\"uller},
   title = {From {I/O} Automata to Timed {I/O} Automata:
            A Solution to the `Generalized Railroad Crossing' in
            {Isabelle}/{HOLCF}},
   pages = {273--289},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Harr,
   author = {J. Harrison},
   title = {A Machine-Checked Theory of Floating Point Arithmetic},
   pages = {113--130},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Hurd,
   author = {J. Hurd},
   title = {Integrating {Gandalf} and {HOL}},
   pages = {311--321},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:KaWP,
   author = {F. Kamm\"uller and M. Wenzel and L. C. Paulson},
   title = {Locales --- A Sectioning Concept for {Isabelle}},
   pages = {149--165},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Krop,
   author = {T. Kropf},
   title = {Recent Advancements in Hardware Verification ---
            How to Make Theorem Proving Fit for an Industrial Usage},
   pages = {1--4},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Matt,
   author = {J. Matthews},
   title = {Recursive Function Definition over Coinductive Types},
   pages = {73--90},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:PfRu,
   author = {H. Pfeifer and H. Rue{\ss}},
   title = {Polytypic Proof Construction},
   pages = {55--72},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Sant,
   author = {T. Santen},
   title = {Isomorphisms --- A Link Between the Shallow and the Deep},
   pages = {37--54},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:ScHo,
   author = {K. Schneider and D. W. Hoffmann},
   title = {A {HOL} Conversion for Translating Linear Time Temporal Logic to
            {\omega}-Automata},
   pages = {255--272},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Stap,
   author = {M. Staples},
   title = {Representing {WP} Semantics in {Isabelle}/{ZF}},
   pages = {239--254},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Syme,
   author = {D. Syme},
   title = {Three Tactic Theorem Proving},
   pages = {203--220},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Volk,
   author = {N. V\"olker},
   title = {Disjoint Sums over Type Classes in {HOL}},
   pages = {5--18},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Wenz,
   author = {M. Wenzel},
   title = {{Isar} --- A Generic Interpretative Approach to Readable Formal
            Proof Documents},
   pages = {167--183},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:XiCT,
   author = {H. Xiong and P. Curzon and S. Tahar},
   title = {Importing {MDG} Verification Results into {HOL}},
   pages = {293--310},
   crossref = {TPHOLs99}}

@InProceedings{TPHOLs99:Zamm,
   author = {V. Zammit},
   title = {On the Implementation of an Extensible Declarative Proof Language},
   pages = {185--202},
   crossref = {TPHOLs99}}

@Proceedings{TPHOLs99,
   title = {Proceedings of the 12th International Conference on
            Theorem Proving in Higher Order Logics (TPHOLs'99)},
   booktitle = {Proceedings of the 12th International Conference on
                Theorem Proving in Higher Order Logics (TPHOLs'99)},
   year = {1999},
   series = {Lecture Notes in Computer Science},
   volume = {1690},
   editor = {Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and
             L. Th\'ery},
   publisher = {Springer},
   address = {Nice, France},
   month = {September}}