Format:
Online-Ressource
ISBN:
9783540459491
,
3540433767
Series Statement:
Lecture Notes in Computer Science 2283
Content:
This textbook-like tutorial is a self-contained introduction to interactive proof, specification, and verification in higher-order logic, using the proof assistant Isabelle 2002. In contrast to existing Isabelle documentation, this book provides a direct route into higher-order logic by bypassing first-order logic and minimizing discussion of meta-theory. Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for higher-order logic; this theorem prover is well suited as a specification and verification system
Additional Edition:
ISBN 9783540433767
Additional Edition:
Buchausg. u.d.T. Nipkow, Tobias, 1958 - Isabelle/HOL Berlin : Springer, 2002 ISBN 3540433767
Language:
English
Subjects:
Computer Science
Keywords:
HOL
;
Isabelle
;
HOL
;
Funktionale Programmierung
;
HOL
;
Formale Methode
;
Aufsatzsammlung
DOI:
10.1007/3-540-45949-9
URL:
Volltext
(lizenzpflichtig)
URL:
Volltext
(lizenzpflichtig)
Author information:
Nipkow, Tobias 1958-
