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

• 2010
• 
  Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry:
  Extending Coq with Imperative Features and Its Application to SAT Verification. ITP 2010: 83-98
• 
  Serge Autexier, Dominik Dietrich:
  A Tactic Language for Declarative Proofs. ITP 2010: 99-114
• 
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
  Programming Language Techniques for Cryptographic Proofs. ITP 2010: 115-130
• 
  Jasmin Christian Blanchette, Tobias Nipkow:
  Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. ITP 2010: 131-146
• 
  Sascha Böhme, Tjark Weber:
  Fast LCF-Style Proof Reconstruction for Z3. ITP 2010: 179-194
• 
  Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
  Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP 2010: 147-162
• 
  Thomas Braibant, Damien Pous:
  An Efficient Coq Tactic for Deciding Kleene Algebras. ITP 2010: 163-178
• 
  David Cachera, David Pichardie:
  A Certified Denotational Abstract Interpreter. ITP 2010: 9-24
• 
  Arthur Charguéraud:
  The Optimal Fixed Point Combinator. ITP 2010: 195-210
• 
  Ernie Cohen, Bert Schirmer:
  From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. ITP 2010: 403-418
• 
  John R. Cowles, Ruben Gamboa:
  Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. ITP 2010: 25-34
• 
  Jean-François Dufourd, Yves Bertot:
  Formal Study of Plane Delaunay Triangulation. ITP 2010: 211-226
• 
  Amy P. Felty, Brigitte Pientka:
  Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. ITP 2010: 227-242
• 
  Anthony C. J. Fox, Magnus O. Myreen:
  A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. ITP 2010: 243-258
• 
  Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen:
  Automated Machine-Checked Hybrid System Safety Proofs. ITP 2010: 259-274
• 
  Joe Hendrix, Deepak Kapur, José Meseguer:
  Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. ITP 2010: 275-290
• 
  Douglas J. Howe:
  Higher-Order Abstract Syntax in Isabelle/HOL. ITP 2010: 481-484
• 
  Brian Huffman, Christian Urban:
  A New Foundation for Nominal Isabelle. ITP 2010: 35-50
• 
  Moa Johansson, Lucas Dixon, Alan Bundy:
  Case-Analysis for Rippling and Inductive Proof. ITP 2010: 291-306
• 
  Chantal Keller, Benjamin Werner:
  Importing HOL Light into Coq. ITP 2010: 307-322
• 
  Gerwin Klein:
  A Formally Verified OS Kernel. Now What? ITP 2010: 1-7
• 
  Alexander Krauss, Andreas Schropp:
  A Mechanized Translation from Higher-Order Logic to Set Theory. ITP 2010: 323-338
• 
  Ramana Kumar, Michael Norrish:
  (Nominal) Unification by Recursive Descent with Triangular Substitutions. ITP 2010: 51-66
• 
  Peter Lammich, Andreas Lochbihler:
  The Isabelle Collections Framework. ITP 2010: 339-354
• 
  Panagiotis Manolios, Daron Vroon:
  Interactive Termination Proofs Using Termination Cores. ITP 2010: 355-370
• 
  William Mansky, Elsa L. Gunter:
  A Framework for Formal Verification of Compiler Optimizations. ITP 2010: 371-386
• 
  Tarek Mhamdi, Osman Hasan, Sofiène Tahar:
  On the Formalization of the Lebesgue Integration Theory in HOL. ITP 2010: 387-402
• 
  Magnus O. Myreen:
  Separation Logic Adapted for Proofs by Rewriting. ITP 2010: 485-489
• 
  Benjamin C. Pierce:
  Proof Assistants as Teaching Assistants: A View from the Trenches. ITP 2010: 8
• 
  Matthieu Sozeau:
  Equations: A Dependent Pattern-Matching Compiler. ITP 2010: 419-434

skipping 6 more matches