12. TPHOLs 1999:
Nice, France
Yves Bertot, Gilles Dowek, André Hirschowitz, C. Paulin, Laurent Théry (Eds.):
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings.
Lecture Notes in Computer Science 1690 Springer 1999, ISBN 3-540-66463-7 
- Thomas Kropf:
Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage.
1-4
- Norbert Völker:
Disjoint Sums over Type Classes in HOL.
5-18
- Stefan Berghofer, Markus Wenzel:
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering.
19-36
- Thomas Santen:
Isomorphisms - A Link Between the Shallow and the Deep.
37-54
- Holger Pfeifer, Harald Rueß:
Polytypic Proof Construction.
55-72
- John Matthews:
Recursive Function Definition over Coinductive Types.
73-90
- Solange Coupet-Grimal, Line Jakubiec:
Hardware Verification Using Co-induction in COQ.
91-108
- Olga Caprotti, Arjeh M. Cohen:
Connecting Proof Checkers and Computer Algebra Using OpenMath.
109-112
- John Harrison:
A Machine-Checked Theory of Floating Point Arithmetic.
113-130
- Venanzio Capretta:
Universal Algebra in Type Theory.
131-148
- Florian Kammüller, Markus Wenzel, Lawrence C. Paulson:
Locales - A Sectioning Concept for Isabelle.
149-166
- Markus Wenzel:
Isar - A Generic Interpretative Approach to Readable Formal Proof Documents.
167-184
- Vincent Zammit:
On the Implementation of an Extensible Declarative Proof Language.
185-202
- Don Syme:
Three Tactic Theorem Proving.
203-220
- Simon Ambler, Roy L. Crole:
Mechanized Operational Semantics via (Co)Induction.
221-238
- Mark Staples:
Representing WP Semantics in Isabelle/ZF.
239-254
- Klaus Schneider, Dirk W. Hoffmann:
A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata.
255-272
- Bernd Grobauer, Olaf Müller:
From I/O Automata to Timed I/O Automata.
273-290
- Dominique Bolignano:
Formal Methods and Security Evaluation (Invited Talk).
291-292
- Haiyan Xiong, Paul Curzon, Sofiène Tahar:
Importing MDG Verification Results into HOL.
293-310
- Joe Hurd:
Integrating Gandalf and HOL.
311-322
- Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger:
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving.
323-340
- Nancy A. Day, Jeffrey J. Joyce:
Symbolic Functional Evaluation.
341-358
Last update Sat May 25 19:10:45 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
