• 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

• 2002
• 
  Simon Ambler, Roy L. Crole, Alberto Momigliano:
  Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. TPHOLs 2002: 13-30
• 
  Gilles Barthe, Pierre Courtieu:
  Efficient Reasoning about Executable Specifications in Coq. TPHOLs 2002: 31-46
• 
  David A. Basin, Stefan Friedrich, Marek Gawkowski:
  Verified Bytecode Model Checkers. TPHOLs 2002: 47-66
• 
  Gertrud Bauer, Tobias Nipkow:
  The 5 Colour Theorem in Isabelle/Isar. TPHOLs 2002: 67-82
• 
  Yves Bertot, Venanzio Capretta, Kuntal Das Barman:
  Type-Theoretic Functional Semantics. TPHOLs 2002: 83-98
• 
  Achim D. Brucker, Burkhart Wolff:
  A Proposal for a Formal OCL Semantics in Isabelle/HOL. TPHOLs 2002: 99-114
• 
  Ricky W. Butler:
  Formal Methods at NASA Langley. TPHOLs 2002: 1-2
• 
  Judicaël Courant:
  Explicit Universes for the Calculus of Constructions. TPHOLs 2002: 115-130
• 
  Jeremy E. Dawson, Rajeev Goré:
  Formalised Cut Admissibility for Display Logic. TPHOLs 2002: 131-147
• 
  Christophe Dehlinger, Jean-François Dufourd:
  Formalizing the Trading Theorem for the Classification of Surfaces. TPHOLs 2002: 148-163
• 
  David Delahaye:
  Free-Style Theorem Proving. TPHOLs 2002: 164-181
• 
  Louise A. Dennis, Alan Bundy:
  A Comparison of Two Proof Critics: Power vs. Robustness. TPHOLs 2002: 182-197
• 
  Amy P. Felty:
  Two-Level Meta-reasoning in Coq. TPHOLs 2002: 198-213
• 
  Michael J. C. Gordon:
  PuzzleTool : An Example of Programming Computation and Deduction. TPHOLs 2002: 214-229
• 
  Gérard P. Huet:
  Higher Order Unification 30 Years Later. TPHOLs 2002: 3-12
• 
  Joe Hurd:
  A Formal Approach to Probabilistic Termination. TPHOLs 2002: 230-245
• 
  Micaela Mayero:
  Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). TPHOLs 2002: 246-262
• 
  Aleksey Nogin:
  Quotient Types: A Modular Approach. TPHOLs 2002: 263-280
• 
  Aleksey Nogin, Jason Hickey:
  Sequent Schema for Derived Rules. TPHOLs 2002: 281-297
• 
  Virgile Prevosto, Damien Doligez, Thérèse Hardin:
  Algebraic Structures and Dependent Records. TPHOLs 2002: 298-313
• 
  Klaus Schneider:
  Proving the Equivalence of Microstep and Macrostep Semantics. TPHOLs 2002: 314-331
• 
  Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu:
  Weakest Precondition for General Recursive Programs Formalized in Coq. TPHOLs 2002: 332-348
• 
  Victor Carreño, César A. Muñoz, Sofiène Tahar:
  Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings. Lecture Notes in Computer Science 2410, Springer 2002, ISBN 3-540-44039-9 [contents]