6 specification and verification system. Isabelle is a generic system for |
6 specification and verification system. Isabelle is a generic system for |
7 implementing logical formalisms, and Isabelle/HOL is the specialization |
7 implementing logical formalisms, and Isabelle/HOL is the specialization |
8 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce |
8 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce |
9 HOL step by step following the equation |
9 HOL step by step following the equation |
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
11 We do not assume that you are familiar with mathematical logic but that |
11 We do not assume that you are familiar with mathematical logic. |
12 you are used to logical and set theoretic notation, such as covered |
12 However, we do assume that |
13 in a good discrete mathematics course~\cite{Rosen-DMA}. |
13 you are used to logical and set theoretic notation, as covered |
14 In contrast, we do assume |
14 in a good discrete mathematics course~\cite{Rosen-DMA}, and |
15 that you are familiar with the basic concepts of functional |
15 that you are familiar with the basic concepts of functional |
16 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}. |
16 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}. |
17 Although this tutorial initially concentrates on functional programming, do |
17 Although this tutorial initially concentrates on functional programming, do |
18 not be misled: HOL can express most mathematical concepts, and functional |
18 not be misled: HOL can express most mathematical concepts, and functional |
19 programming is just one particularly simple and ubiquitous instance. |
19 programming is just one particularly simple and ubiquitous instance. |