• Archive Formal Proofs

  • Referenced in 181 articles [sw28613]
  • Isabelle’s Archive of Formal Proofs (AFP): Mining the Archive of Formal Proofs. The Archive ... Formal Proofs is a vast collection of computer-checked proofs developed using the proof assistant ... archive, looking at various properties of the proof developments, including size, dependencies, and proof style ... gives some insights into the nature of formal proofs...
  • Secondary Sylow

  • Referenced in 3 articles [sw29536]
  • Archive of formal proofs: Secondary Sylow Theorems. These theories extend the existing proof...
  • Regular_Algebras

  • Referenced in 3 articles [sw32237]
  • relationships between these classes, formalise a soundness proof for the smallest class (Salomaa ... Kleene algebra hierarchy in the Archive of Formal Proofs; we have not aimed...
  • Cofinitary Group

  • Referenced in 2 articles [sw29535]
  • Archive of formal proofs: An Example of a Cofinitary Group in Isabelle/HOL. We formalize...
  • Vector Spaces

  • Referenced in 2 articles [sw28662]
  • vector spaces. The proofs are standard; the proofs of the replacement theorem and rank-nullity ... existing development in the Archive of Formal Proof (originally using type classes, now using...
  • Landau Symbols

  • Referenced in 2 articles [sw29537]
  • Archive of formal proofs: Landau Symbols. This entry provides Landau symbols to describe and reason...
  • Jordan Hölder

  • Referenced in 1 article [sw29552]
  • Archive of formal proofs: The Jordan-Hölder Theorem. This submission contains theories that lead...
  • Median-of-Medians

  • Referenced in 1 article [sw29538]
  • Archive of formal proof: The Median-of-Medians Selection Algorithm. This entry provides an executable...
  • Slicing

  • Referenced in 1 article [sw29542]
  • Archive of formal proofs: Towards Certified Slicing. Slicing is a widely-used technique with applications...
  • Volpano Smith

  • Referenced in 1 article [sw29543]
  • Archive of formal proofs: A Correctness Proof for the Volpano/Smith Security Typing System. The Volpano/Smith/Irvine...
  • EthVer

  • Referenced in 1 article [sw42609]
  • tool for formal verification of models. As a proof of concept, we use our tool ... Micropayments for decentralized currencies'', Preprint, Cryptology ePrint Archive, url{https://eprint.iacr.org/2016/332}].$...
  • Matlab

  • Referenced in 13702 articles [sw00558]
  • MATLAB® is a high-level language and interactive...
  • MACSYMA

  • Referenced in 721 articles [sw01209]
  • Macsyma is a general purpose symbolic-numerical-graphical...
  • PERL

  • Referenced in 274 articles [sw01225]
  • Programming Perl. Perl is a language for easily...
  • Algolib

  • Referenced in 3 articles [sw04111]
  • Algolib: The Algorithms Project’s Library and Other...
  • GitHub

  • Referenced in 2760 articles [sw23170]
  • GitHub (originally known as Logical Awesome LLC)[3...