• case-insensitive prefix search: default
  e.g., sig matches "SIGIR" as well as "signal"
• exact word search: append dollar sign ($) to word
  e.g., graph$ matches "graph", but not "graphics"
• boolean and: separate words by space
  e.g., codd model
• boolean or: connect words by pipe symbol (|)
  e.g., graph|network

Update May 7, 2017: Please note that we had to disable the phrase search operator (.) and the boolean not operator (-) due to technical problems. For the time being, phrase search queries will yield regular prefix search result, and search terms preceded by a minus will be interpreted as regular (positive) search terms.

found 24 matches

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