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

• 2020
• 
  Andrew W. Appel, Yves Bertot:
  C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13(1): 1-16 (2020)
• 
  Andrew W. Appel, Yves Bertot:
  Corrigendum: C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13(1) (2020)
• 2019
• 
  Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto:
  LF+ in Coq for "fast and loose" reasoning. J. Formaliz. Reason. 12(1): 11-51 (2019)
• 
  Ranganathan Padmanabhan, Yang Zhang:
  Commutativity Theorems in Groups with Power-like Maps. J. Formaliz. Reason. 12(1): 1-10 (2019)
• 
  Raphaël Rieu-Helft:
  A Why3 proof of GMP algorithms. J. Formaliz. Reason. 12(1): 53-97 (2019)
• 2018
• 
  Reynald Affeldt, Cyril Cohen, Damien Rouhling:
  Formalization Techniques for Asymptotic Reasoning in Classical Analysis. J. Formaliz. Reason. 11(1): 43-76 (2018)
• 
  Pierre Lescanne:
  Dependent Types for Extensive Games. J. Formaliz. Reason. 11(1): 1-17 (2018)
• 
  César A. Muñoz, Anthony J. Narkawicz, Aaron Dutle:
  A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision. J. Formaliz. Reason. 11(1): 19-41 (2018)
• 2017
• 
  Alexander Bagnall, Samuel Merten, Gordon Stewart:
  A Library for Algorithmic Game Theory in Ssreflect/Coq. J. Formaliz. Reason. 10(1): 67-95 (2017)
• 
  James Chapman, Tarmo Uustalu, Niccolò Veltri:
  Formalizing Restriction Categories. J. Formaliz. Reason. 10(1): 1-36 (2017)
• 
  Ran Chen, Martin Clochard, Claude Marché:
  A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. J. Formaliz. Reason. 10(1): 51-66 (2017)
• 
  Daniel de Rauglaudre:
  Formal Proof of Banach-Tarski Paradox. J. Formaliz. Reason. 10(1): 37-49 (2017)
• 2016
• 
  Mark Miles Adams:
  Proof Auditing Formalised Mathematics. J. Formaliz. Reason. 9(1): 3-32 (2016)
• 
  Robin Denis Arthan:
  Now f is continuous (exercise!). J. Formaliz. Reason. 9(1): 33-52 (2016)
• 
  Arnon Avron, Liron Cohen:
  Formalizing Scientifically Applicable Mathematics in a Definitional Framework. J. Formaliz. Reason. 9(1): 53-70 (2016)
• 
  Michael Beeson:
  Mixing Computations and Proofs. J. Formaliz. Reason. 9(1): 71-99 (2016)
• 
  Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
  Hammering towards QED. J. Formaliz. Reason. 9(1): 101-148 (2016)
• 
  Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger:
  Theorema 2.0: Computer-Assisted Natural-Style Mathematics. J. Formaliz. Reason. 9(1): 149-185 (2016)
• 
  Mario Carneiro:
  Conversion of HOL Light proofs into Metamath. J. Formaliz. Reason. 9(1): 187-200 (2016)
• 
  José Grimm:
  Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers. J. Formaliz. Reason. 9(2): 1-52 (2016)
• 
  John Harrison, Josef Urban, Freek Wiedijk:
  Preface: Twenty Years of the QED Manifesto. J. Formaliz. Reason. 9(1): 1-2 (2016)
• 
  Michael Kohlhase, Florian Rabe:
  QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge. J. Formaliz. Reason. 9(1): 201-234 (2016)
• 
  Yuhui Lin, Gudmund Grov, Rob Arthan:
  Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. J. Formaliz. Reason. 9(2): 69-130 (2016)
• 
  Alexander V. Lyaletski:
  Mathematical Text Processing in EA-style: a Sequent Aspect. J. Formaliz. Reason. 9(1): 235-264 (2016)
• 
  Kevin Quirin, Nicolas Tabareau:
  Lawvere-Tierney sheafification in Homotopy Type Theory. J. Formaliz. Reason. 9(2): 131-161 (2016)
• 
  Marcus Vinícius Midena Ramos, José Carlos Bacelar Almeida, Nelma Moreira, Ruy José Guerra Barretto de Queiroz:
  Formalization of the pumping lemma for context-free languages. J. Formaliz. Reason. 9(2): 53-68 (2016)
• 2015
• 
  Benedikt Ahrens:
  Initiality for Typed Syntax and Semantics. J. Formaliz. Reason. 8(2): 1-155 (2015)
• 
  Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka:
  Programming type-safe transformations using higher-order abstract syntax. J. Formaliz. Reason. 8(1): 49-91 (2015)
• 
  Mitchell Buckley:
  A formal verification of the theory of parity complexes. J. Formaliz. Reason. 8(1): 25-48 (2015)
• 
  Ferruccio Guidi:
  Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions. J. Formaliz. Reason. 8(1): 93-116 (2015)

skipping 34 more matches