12. TPHOLs 1999: Nice, France

@proceedings{DBLP:conf/tphol/1999,
  editor    = {Yves Bertot and
               Gilles Dowek and
               Andr{\'e} Hirschowitz and
               C. Paulin and
               Laurent Th{\'e}ry},
  title     = {Theorem Proving in Higher Order Logics, 12th International Conference,
               TPHOLs'99, Nice, France, September, 1999, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1690},
  year      = {1999},
  isbn      = {3-540-66463-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

• Thomas Kropf:
  Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage. 1-4
  Electronic Edition (Springer LINK) BibTeX
• Norbert Völker:
  Disjoint Sums over Type Classes in HOL. 5-18
  Electronic Edition (Springer LINK) BibTeX
• Stefan Berghofer, Markus Wenzel:
  Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. 19-36
  Electronic Edition (Springer LINK) BibTeX
• Thomas Santen:
  Isomorphisms - A Link Between the Shallow and the Deep. 37-54
  Electronic Edition (Springer LINK) BibTeX
• Holger Pfeifer, Harald Rueß:
  Polytypic Proof Construction. 55-72
  Electronic Edition (Springer LINK) BibTeX
• John Matthews:
  Recursive Function Definition over Coinductive Types. 73-90
  Electronic Edition (Springer LINK) BibTeX
• Solange Coupet-Grimal, Line Jakubiec:
  Hardware Verification Using Co-induction in COQ. 91-108
  Electronic Edition (Springer LINK) BibTeX
• Olga Caprotti, Arjeh M. Cohen:
  Connecting Proof Checkers and Computer Algebra Using OpenMath. 109-112
  Electronic Edition (Springer LINK) BibTeX
• John Harrison:
  A Machine-Checked Theory of Floating Point Arithmetic. 113-130
  Electronic Edition (Springer LINK) BibTeX
• Venanzio Capretta:
  Universal Algebra in Type Theory. 131-148
  Electronic Edition (Springer LINK) BibTeX
• Florian Kammüller, Markus Wenzel, Lawrence C. Paulson:
  Locales - A Sectioning Concept for Isabelle. 149-166
  Electronic Edition (Springer LINK) BibTeX
• Markus Wenzel:
  Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. 167-184
  Electronic Edition (Springer LINK) BibTeX
• Vincent Zammit:
  On the Implementation of an Extensible Declarative Proof Language. 185-202
  Electronic Edition (Springer LINK) BibTeX
• Don Syme:
  Three Tactic Theorem Proving. 203-220
  Electronic Edition (Springer LINK) BibTeX
• Simon Ambler, Roy L. Crole:
  Mechanized Operational Semantics via (Co)Induction. 221-238
  Electronic Edition (Springer LINK) BibTeX
• Mark Staples:
  Representing WP Semantics in Isabelle/ZF. 239-254
  Electronic Edition (Springer LINK) BibTeX
• Klaus Schneider, Dirk W. Hoffmann:
  A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata. 255-272
  Electronic Edition (Springer LINK) BibTeX
• Bernd Grobauer, Olaf Müller:
  From I/O Automata to Timed I/O Automata. 273-290
  Electronic Edition (Springer LINK) BibTeX
• Dominique Bolignano:
  Formal Methods and Security Evaluation (Invited Talk). 291-292
  Electronic Edition (Springer LINK) BibTeX
• Haiyan Xiong, Paul Curzon, Sofiène Tahar:
  Importing MDG Verification Results into HOL. 293-310
  Electronic Edition (Springer LINK) BibTeX
• Joe Hurd:
  Integrating Gandalf and HOL. 311-322
  Electronic Edition (Springer LINK) BibTeX
• Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger:
  Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. 323-340
  Electronic Edition (Springer LINK) BibTeX
• Nancy A. Day, Jeffrey J. Joyce:
  Symbolic Functional Evaluation. 341-358
  Electronic Edition (Springer LINK) BibTeX