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

• 2019
• 
  Lukasz Czajka:
  First-Order Guarded Coinduction in Coq. ITP 2019: 14:1-14:18
• 
  Julian Brunner, Benedikt Seidl, Salomon Sickert:
  A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. ITP 2019: 11:1-11:19
• 
  Akihisa Yamada, Jérémy Dubut:
  Complete Non-Orders and Fixed Points. ITP 2019: 30:1-30:16
• 
  Yannick Forster, Fabian Kunze:
  A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. ITP 2019: 17:1-17:19
• 
  Mohammad Abdulaziz, Charles Gretton, Michael Norrish:
  A Verified Compositional Algorithm for AI Planning. ITP 2019: 4:1-4:19
• 
  Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka:
  Proving Tree Algorithms for Succinct Data Structures. ITP 2019: 5:1-5:19
• 
  June Andronick:
  A Million Lines of Proof About a Moving Target (Invited Talk). ITP 2019: 1:1-1:1
• 
  Jeremy Avigad, Mario Carneiro, Simon Hudon:
  Data Types as Quotients of Polynomial Functors. ITP 2019: 6:1-6:19
• 
  Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher:
  The DPRM Theorem in Isabelle (Short Paper). ITP 2019: 33:1-33:7
• 
  Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux:
  Primitive Floats in Coq. ITP 2019: 7:1-7:20
• 
  Florent Bréhard, Assia Mahboubi, Damien Pous:
  A Certificate-Based Approach to Formally Verified Approximations. ITP 2019: 8:1-8:19
• 
  Chad E. Brown, Cezary Kaliszyk, Karol Pak:
  Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ITP 2019: 9:1-9:16
• 
  Matthias Brun, Dmitriy Traytel:
  Generic Authenticated Data Structures, Formally. ITP 2019: 10:1-10:18
• 
  Kevin Buzzard:
  What Makes a Mathematician Tick? (Invited Talk). ITP 2019: 2:1-2:1
• 
  Mario Carneiro:
  Formalizing Computability Theory via Partial Recursive Functions. ITP 2019: 12:1-12:17
• 
  Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry:
  Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. ITP 2019: 13:1-13:19
• 
  Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis:
  Formalizing the Solution to the Cap Set Problem. ITP 2019: 15:1-15:19
• 
  Martin Dixon:
  An Increasing Need for Formality (Invited Talk). ITP 2019: 3:1-3:1
• 
  Manuel Eberl:
  Nine Chapters of Analytic Number Theory in Isabelle/HOL. ITP 2019: 16:1-16:19
• 
  Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier:
  Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. ITP 2019: 18:1-18:20
• 
  Jesse Michael Han, Floris van Doorn:
  A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. ITP 2019: 19:1-19:19
• 
  Maximilian P. L. Haslbeck, Peter Lammich:
  Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. ITP 2019: 20:1-20:18
• 
  Fabian Immler, Jonas Rädle, Makarius Wenzel:
  Virtualization of HOL4 in Isabelle. ITP 2019: 21:1-21:18
• 
  Jan Jakubuv, Josef Urban:
  Hammering Mizar by Learning Clause Guidance (Short Paper). ITP 2019: 34:1-34:8
• 
  Cezary Kaliszyk, Karol Pak:
  Declarative Proof Translation (Short Paper). ITP 2019: 35:1-35:7
• 
  Peter Lammich:
  Generating Verified LLVM from Isabelle/HOL. ITP 2019: 22:1-22:19
• 
  Peter Lammich, Tobias Nipkow:
  Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. ITP 2019: 23:1-23:18
• 
  Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux:
  A Verified LL(1) Parser Generator. ITP 2019: 24:1-24:18
• 
  Mihir Parang Mehta, William R. Cook:
  Binary-Compatible Verification of Filesystems with ACL2. ITP 2019: 25:1-25:18
• 
  Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen:
  Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. ITP 2019: 32:1-32:19

skipping 8 more matches