Isabelle/HOL

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.


References in zbMATH (referenced in 702 articles , 2 standard articles )

Showing results 1 to 20 of 702.
Sorted by year (citations)

1 2 3 ... 34 35 36 next

  1. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019-2019)
  2. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019-2019)
  3. Schmidt-Schauß, Manfred; Sabel, David; Kutz, Yunus D. K.: Nominal unification with atom-variables (2019-2019)
  4. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  5. Foster, Simon; Cavalcanti, Ana; Woodcock, Jim; Zeyda, Frank: Unifying theories of time with generalised reactive processes (2018)
  6. Maggesi, Marco: A formalization of metric spaces in HOL light (2018)
  7. Steffen, Bernhard; Rüthing, Oliver; Huth, Michael: Mathematical foundations of advanced informatics. Volume 1. Inductive approaches (2018)
  8. Struth, Georg: Hoare semigroups (2018)
  9. Albert, Elvira; Bezirgiannis, Nikolaos; de Boer, Frank; Martin-Martin, Enrique: A formal, resource consumption-preserving translation of actors to Haskell (2017)
  10. Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
  11. Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke: A formally verified proof of the central limit theorem (2017)
  12. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal $\alpha$-equivalence with A and AC function symbols (2017)
  13. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2017)
  14. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  15. Berghammer, Rudolf; Stucke, Insa; Winter, Michael: Using relation-algebraic means and tool support for investigating and computing bipartitions (2017)
  16. Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy: Foundational (co)datatypes and (co)recursion for higher-order logic (2017)
  17. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  18. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  19. Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel: A lambda-free higher-order recursive path order (2017)
  20. Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)

1 2 3 ... 34 35 36 next