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 1018 articles , 2 standard articles )

Showing results 981 to 1000 of 1018.
Sorted by year (citations)

previous 1 2 3 ... 48 49 50 51 next

  1. Boulton, Richard J. (ed.); Jackson, Paul B. (ed.): Theorem proving in higher order logics. 14th international conference, TPHOLs 2001, Edinburgh, Scotland, GB, September 3--6, 2001. Proceedings (2001)
  2. Gay, Simon J.: A framework for the formalisation of pi calculus type systems in Isabelle/HOL (2001)
  3. Helke, Steffen; Kammüller, Florian: Representing hierarchical automata in interactive theorem provers (2001)
  4. Helke, Steffen; Santen, Thomas: Mechanized analysis of behavioral conformance in the Eiffel base libraries (2001)
  5. Hemer, David; Hayes, Ian; Strooper, Paul: Refinement calculus for logic programming in Isabelle/HOL (2001)
  6. Klein, Gerwin; Nipkow, Tobias: Verified lightweight bytecode verification (2001)
  7. Mattolini, Riccardo; Nesi, Paolo: An Interval Logic for Real-Time System Specification (2001) ioport
  8. Miculan, Marino: Developing (meta)theory of (\lambda)-calculus in the theory of contexts (2001)
  9. Nipkow, Tobias: Verified bytecode verifiers (2001)
  10. Nipkow, Tobias: More Church-Rosser proofs (in Isabelle/HOL) (2001)
  11. Rasmussen, Thomas Marthedal: An inductive approach to formalizing notions of number theory proofs (2001)
  12. Röckl, Christine: A first-order syntax for the (\pi)-calculus in Isabelle/HOL using permutations (2001)
  13. Röckl, Christine; Hirschkoff, Daniel; Berghofer, Stefan: Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the (\pi)-calculus and mechanizing the theory of contexts (2001)
  14. Vestergaard, René; Brotherston, James: A formalised first-order confluence proof for the (\lambda)-calculus using one-sorted variable names (Barendregt was right after all . . . almost) (2001)
  15. Vestergaard, René; Brotherston, James: The mechanisation of Barendregt-style equational proofs (the residual perspective) (2001)
  16. von Oheimb, David: Hoare logic for Java in Isabelle/HOL (2001)
  17. Aagaard, Mark (ed.); Harrison, John (ed.): Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings (2000)
  18. Bauer, Gertrud; Wenzel, Markus: Computer-assisted mathematics at work. The Hahn-Banach theorem in Isabelle/Isar (2000)
  19. Dubois, Catherine: Proving ML type soundness within Coq (2000)
  20. Fleuriot, Jacques D.: On the mechanization of real analysis in Isabelle/HOL (2000)

previous 1 2 3 ... 48 49 50 51 next