default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID12th TPHOLs 1999: Nice, France
- Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry:
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 D. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-22 03:45 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
