• CSP-prover

  • Referenced in 15 articles [sw11465]
  • based on the generic theorem prover Isabelle, using the logic HOL-Complex. Within this logic...
  • Poly/ML

  • Referenced in 11 articles [sw11353]
  • Paulson who used it to develop the Isabelle theorem prover. It was licensed by Cambridge...
  • miz3

  • Referenced in 11 articles [sw18631]
  • styles have been combined before in the Isabelle, Ssreflect and Matita systems. Our approach...
  • PIDE

  • Referenced in 10 articles [sw06404]
  • connect LCF-style provers like Isabelle...
  • Isabelle/UTP

  • Referenced in 10 articles [sw21184]
  • results from well-supported mathematical structures in Isabelle to proofs about UTP theories. Additionally...
  • Zeno

  • Referenced in 9 articles [sw07735]
  • successful, it converts the proof into Isabelle code. Zeno searches for a proof tree...
  • RALL

  • Referenced in 9 articles [sw08505]
  • Logic), based on the generic theorem prover Isabelle. On the one hand, the system...
  • Presburger Automata

  • Referenced in 9 articles [sw28603]
  • arithmetic, which is efficiently executable thanks to Isabelle’s code generator. With this work...
  • Eisbach

  • Referenced in 5 articles [sw13077]
  • Isabelle proof method language. Machine-checked proofs are becoming ever-larger, presenting an increasing maintenance ... challenge. Isabelle’s most popular language interface, Isar, is attractive for new users, and powerful ... present Eisbach, a proof method language for Isabelle, which aims to fill this...
  • IsaWin

  • Referenced in 8 articles [sw04899]
  • instantiated to an interface for Isabelle, called IsaWin, as well as to a tailored tool...
  • VeriML

  • Referenced in 8 articles [sw13522]
  • Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance...
  • Berlekamp Zassenhaus

  • Referenced in 8 articles [sw28596]
  • Isabelle/HOL, we formalize the whole algorithm using Isabelle’s recent addition of local type definitions...
  • Density Compiler

  • Referenced in 5 articles [sw28659]
  • this language within the theorem prover Isabelle and give a formal proof of its soundness ... source and target language. Together with Isabelle’s code generation for inductive predicates, this yields...
  • Rabinizer

  • Referenced in 7 articles [sw21008]
  • algorithm implemented has been proven correct in Isabelle. For questions please contact Jan Kretinsky...
  • Ergo 6

  • Referenced in 6 articles [sw18584]
  • generic interactive theorem prover, similar to Isabelle, but with better support for proving schematic theorems...
  • Speedith

  • Referenced in 6 articles [sw19455]
  • steps within established proof assistants such as Isabelle. We describe the general structure of Speedith...
  • Coinductive

  • Referenced in 6 articles [sw28537]
  • Isabelle Coinductive: This article collects formalisations of general-purpose coinductive data types and sets. Currently...
  • IsaFoR

  • Referenced in 5 articles [sw10106]
  • Termination of Isabelle functions via termination of rewriting. We show how to automate termination proofs...