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

• 2018
• 
  Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples:
  Towards verifying ethereum smart contract bytecode in Isabelle/HOL. CPP 2018: 66-77
• 
  Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
  Proofs in conflict-driven theory combination. CPP 2018: 186-200
• 
  Kaustuv Chaudhuri:
  A two-level logic perspective on (simultaneous) substitutions. CPP 2018: 280-292
• 
  Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
  Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). CPP 2018: 2-13
• 
  Boris Djalal:
  A constructive formalisation of Semi-algebraic sets and functions. CPP 2018: 240-251
• 
  Christian Doczkal, Joachim Bard:
  Completeness and decidability of converse PDL in the constructive type theory of Coq. CPP 2018: 42-52
• 
  Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak:
  Formal proof of polynomial-time complexity with quasi-interpretations. CPP 2018: 146-157
• 
  Denis Firsov, Aaron Stump:
  Generic derivation of induction for impredicative encodings in Cedille. CPP 2018: 215-227
• 
  Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich:
  A verified SAT solver with watched literals using imperative HOL. CPP 2018: 158-171
• 
  Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide:
  Finite sets in homotopy type theory. CPP 2018: 201-214
• 
  Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin:
  A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. CPP 2018: 130-145
• 
  Jonas Kaiser, Steven Schäfer, Kathrin Stark:
  Binder aware recursion over well-scoped de Bruijn syntax. CPP 2018: 293-306
• 
  Cezary Kaliszyk, Julian Parsert:
  Formal microeconomic foundations and the first welfare theorem. CPP 2018: 91-101
• 
  Dominik Kirst, Gert Smolka:
  Large model constructions for second-order ZF in dependent type theory. CPP 2018: 228-239
• 
  Sergueï Lenglet, Alan Schmitt:
  HOπ in Coq. CPP 2018: 252-265
• 
  Craig McLaughlin, James McKinna, Ian Stark:
  Triangulating context lemmas. CPP 2018: 102-114
• 
  Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman:
  Œuf: minimizing the Coq extraction TCB. CPP 2018: 172-185
• 
  Brigitte Pientka:
  POPLMark reloaded: mechanizing logical relations proofs (invited talk). CPP 2018: 1
• 
  George Pîrlea, Ilya Sergey:
  Mechanising blockchain consensus. CPP 2018: 78-90
• 
  Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman:
  Adapting proof automation to adapt proofs. CPP 2018: 115-129
• 
  Damien Rouhling:
  A formal proof in Coq of a control function for the inverted pendulum. CPP 2018: 28-41
• 
  Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich:
  Total Haskell is reasonable Coq. CPP 2018: 14-27
• 
  Conrad Watt:
  Mechanising and verifying the WebAssembly specification. CPP 2018: 53-65
• 
  Pawel Wieczorek, Dariusz Biernacki:
  A Coq formalization of normalization by evaluation for Martin-Löf type theory. CPP 2018: 266-279
• 
  June Andronick, Amy P. Felty:
  Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018. ACM 2018, ISBN 978-1-4503-5586-5 [contents]