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

• 2000
• 
  Antonia Balaa, Yves Bertot:
  Fix-Point Equations for Well-Founded Recursion in Type Theory. TPHOLs 2000: 1-16
• 
  Bruno Barras:
  Programming and Computing in HOL. TPHOLs 2000: 17-37
• 
  Stefan Berghofer, Tobias Nipkow:
  Proof Terms for Simply Typed Higher Order Logic. TPHOLs 2000: 38-52
• 
  Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic:
  Routing Information Protocol in HOL/SPIN. TPHOLs 2000: 53-72
• 
  Venanzio Capretta:
  Recursive Families of Inductive Types. TPHOLs 2000: 73-89
• 
  Victor Carreño, César A. Muñoz:
  Aircraft Trajectory Modeling and Altering Algorithm Verification. TPHOLs 2000: 90-105
• 
  Robert P. Colwell, Bob Brennan:
  Intel's Formal Verification Experience on the Willamette Development. TPHOLs 2000: 106-107
• 
  Ewen Denney:
  A Prototype Proof Translator from HOL to Coq. TPHOLs 2000: 108-125
• 
  Catherine Dubois:
  Proving ML Type Soundness Within Coq. TPHOLs 2000: 126-144
• 
  Jacques D. Fleuriot:
  On the Mechanization of Real Analysis in Isabelle/HOL. TPHOLs 2000: 145-161
• 
  Herman Geuvers, Freek Wiedijk, Jan Zwanenburg:
  Equational Reasoning via Partial Reflection. TPHOLs 2000: 162-178
• 
  Michael J. C. Gordon:
  Reachability Programming in HOL98 Using BDDs. TPHOLs 2000: 179-196
• 
  Hanne Gottliebsen:
  Transcendental Functions and Continuity Checking in PVS. TPHOLs 2000: 197-214
• 
  Jim Grundy:
  Verified Optimizations for the Intel IA-64 Architecture. TPHOLs 2000: 215-232
• 
  John Harrison:
  Formal Verification of IA-64 Division Algorithms. TPHOLs 2000: 233-251
• 
  Jason Hickey, Aleksey Nogin:
  Fast Tactic-Based Theorem Proving. TPHOLs 2000: 252-267
• 
  Martin Hofmann, Francis Tang:
  Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover. TPHOLs 2000: 268-282
• 
  M. Randall Holmes:
  A Strong and Mechanizable Grand Logic. TPHOLs 2000: 283-300
• 
  Marieke Huisman, Bart Jacobs:
  Inheritance in Higher Order Logic: Modeling and Reasoning. TPHOLs 2000: 301-319
• 
  Paul B. Jackson:
  Total-Correctness Refinement for Sequential Reactive Systems. TPHOLs 2000: 320-337
• 
  Roope Kaivola, Mark D. Aagaard:
  Divider Circuit Verification with Model Checking and Theorem Proving. TPHOLs 2000: 338-355
• 
  Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin:
  Specification and Verification of a Steam-Boiler with Signal-Coq. TPHOLs 2000: 356-371
• 
  Linas Laibinis, Joakim von Wright:
  Functional Procedures in Higher-Order Logic. TPHOLs 2000: 372-387
• 
  Pierre Letouzey, Laurent Théry:
  Formalizing Stålmarck's Algorithm in Coq. TPHOLs 2000: 388-405
• 
  Christoph Lüth, Burkhart Wolff:
  TAS - A Generic Window Inference System. TPHOLs 2000: 406-423
• 
  Stephan Merz:
  Weak Alternating Automata in Isabelle/HOL. TPHOLs 2000: 424-441
• 
  Robin Milner:
  Graphical Theories of Interactive Systems: Can a Proof Assistant Help? TPHOLs 2000: 442
• 
  Abdel Mokkedem, Tim Leonard:
  Formal Verification of the Alpha 21364 Network Protocol. TPHOLs 2000: 443-461
• 
  Robert Pollack:
  Dependently Typed Records for Representing Mathematical Structure. TPHOLs 2000: 462-479
• 
  Bernhard Reus, Tatjana Hein:
  Towards a Machine-Checked Java Specification Book. TPHOLs 2000: 480-497

skipping 4 more matches