• 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 23 matches

• 1997
• 
  Sten Agerholm, Jacob Frost:
  An Isabelle-Based Theorem Prover for VDM-SL. TPHOLs 1997: 1-16
• 
  James H. Andrews:
  Executing Formal Specifications by Translation to Higher Order Logic Programming. TPHOLs 1997: 17-32
• 
  Myla Archer, Constance L. Heitmeyer:
  Human-Style Theorem Proving Using PVS. TPHOLs 1997: 33-48
• 
  Albert John Camilleri:
  A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processor. TPHOLs 1997: 49-67
• 
  Boutheina Chetali, Barbara Heyd:
  Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis. TPHOLs 1997: 69-85
• 
  Robert L. Constable:
  ML Programming in Constructive Type Theory (abstract). TPHOLs 1997: 87
• 
  Marco Devillers, W. O. David Griffioen, Olaf Müller:
  Possibly Infinite Sequences in Theorem Provers: A Comparative Study. TPHOLs 1997: 89-104
• 
  Gilles Dowek:
  Proof Normalization for a First-Order Formulation of Higher-Order Logic. TPHOLs 1997: 105-119
• 
  Bruno Dutertre, Steve A. Schneider:
  Using a PVS Embedding of CSP to Verify Authentication Protocols. TPHOLs 1997: 121-136
• 
  John Harrison:
  Verifying the Accuracy of Polynomial Approximations in HOL. TPHOLs 1997: 137-152
• 
  Daniel Hirschkoff:
  A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions. TPHOLs 1997: 153-169
• 
  Deepak Kapur:
  Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification. TPHOLs 1997: 171-182
• 
  Thomas Långbacka, Joakim von Wright:
  Refining Reactive Systems in HOL Using Action Systems. TPHOLs 1997: 183-197
• 
  Takahisa Mohri:
  On Formalization of Bicategory Theory. TPHOLs 1997: 199-214
• 
  Wolfgang Naraschewski:
  Towards an Object-Oriented Progification Language. TPHOLs 1997: 215-230
• 
  Doron A. Peled:
  Verification for Robust Specification. TPHOLs 1997: 231-241
• 
  Thomas Santen:
  A Theory of Structured Model-Based Specifications in Isabelle/HOL. TPHOLs 1997: 243-258
• 
  Martin Simons:
  Proof Presentation for Isabelle. TPHOLs 1997: 259-274
• 
  Konrad Slind:
  Derivation and Use of Induction Schemes in Higher-Order Logic. TPHOLs 1997: 275-290
• 
  Oscar Slotosch:
  Higher Order Quotients and their Implementation in Isabelle HOL. TPHOLs 1997: 291-306
• 
  Markus Wenzel:
  Type Classes and Overloading in Higher-Order Logic. TPHOLs 1997: 307-322
• 
  Vincent Zammit:
  A Comparative Study of Coq and HOL. TPHOLs 1997: 323-337
• 
  Elsa L. Gunter, Amy P. Felty:
  Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings. Lecture Notes in Computer Science 1275, Springer 1997, ISBN 3-540-63379-0 [contents]