This paper introduces interactive theorem proving with the Isabelle/HOL system . The following topics are covered:
• Verified functional programming: The logic HOL contains an ML-style functional programming language. It is shown how to verify functional programs in this language by induction and simplification.
• Predicate logic: Formulas of predicate logic and set theory are introduced, together with methods for proof automation.
• Inductively defined predicates.
• Structured proofs: We introduce the proof language Isar and show how to write structured proofs that are readable by both the machine and the human.
We assume basic familiarity with some functional programming language of the ML or Haskell family, in particular with recursive data types and pattern matching. No specific background in logic is necessary beyond the ability to read predicate logic formulas.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 email@example.com
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 firstname.lastname@example.org