• 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

• 2003
• 
  Jean-Raymond Abrial, Dominique Cansell:
  Click'n Prove: Interactive Proofs within Set Theory. TPHOLs 2003: 1-24
• 
  Hasan Amjad:
  Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. TPHOLs 2003: 171-187
• 
  June Andronick, Boutheina Chetali, Olivier Ly:
  Using Coq to Verify Java Card Applet Isolation Properties. TPHOLs 2003: 335-351
• 
  Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson:
  Verifying Second-Level Security Protocols. TPHOLs 2003: 352-366
• 
  David Cachera, David Pichardie:
  Embedding of Systems of Affine Recurrence Equations in Coq. TPHOLs 2003: 155-170
• 
  Jacek Chrzaszcz:
  Implementing Modules in the Coq System. TPHOLs 2003: 270-286
• 
  Luís Cruz-Filipe, Bas Spitters:
  Program Extraction from Large Proof Developments. TPHOLs 2003: 205-220
• 
  Peter Dybjer, Qiao Haiyan, Makoto Takeyama:
  Combining Testing and Proving in Dependent Type Theory. TPHOLs 2003: 188-203
• 
  Anthony C. J. Fox:
  Formal Specification and Verification of ARM6. TPHOLs 2003: 25-40
• 
  Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, Xin Yu:
  MetaPRL - A Modular Logical Environment. TPHOLs 2003: 287-303
• 
  Deepak Kapur, Nikita A. Sakhanenko:
  Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions. TPHOLs 2003: 136-154
• 
  Gerwin Klein, Martin Wildmoser:
  Verified Bytecode Subroutines. TPHOLs 2003: 55-70
• 
  Sava Krstic, John Matthews:
  Inductive Invariants for Nested Recursion. TPHOLs 2003: 253-269
• 
  Nicolas Magaud:
  Changing Data Representation within the Coq System. TPHOLs 2003: 87-102
• 
  Laura I. Meikle, Jacques D. Fleuriot:
  Formalizing Hilbert's Grundlagen in Isabelle/Isar. TPHOLs 2003: 319-334
• 
  Dale Miller:
  Reasoning about Proof Search Specifications: An Abstract. TPHOLs 2003: 204
• 
  Michael Norrish:
  Complete Integer Decision Procedures as Derived Rules in HOL. TPHOLs 2003: 71-86
• 
  Claire Louise Quigley:
  A Programming Logic for Java Bytecode Programs. TPHOLs 2003: 41-54
• 
  Jason Reed:
  Extending Higher-Order Unification to Support Proof Irrelevance. TPHOLs 2003: 238-252
• 
  Carsten Schürmann, Frank Pfenning:
  A Coverage Checking Algorithm for LF. TPHOLs 2003: 120-135
• 
  Konrad Slind, Joe Hurd:
  Applications of Polytypism in Theorem Proving. TPHOLs 2003: 103-119
• 
  Laurent Théry:
  Proving Pearl: Knuth's Algorithm for Prime Numbers. TPHOLs 2003: 304-318
• 
  Freek Wiedijk, Jan Zwanenburg:
  First Order Logic with Domain Conditions. TPHOLs 2003: 221-237
• 
  David A. Basin, Burkhart Wolff:
  Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings. Lecture Notes in Computer Science 2758, Springer 2003, ISBN 3-540-40664-6 [contents]