**Isabelle/HOL: A Proof Assistant for Higher-Order Logic**

by T. Nipkow, L.C. Paulson, M. Wenzel

**Publisher**: Springer 2010**ISBN/ASIN**: 3540433767**ISBN-13**: 9783540433767**Number of pages**: 223

**Description**:

This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle. It is a tutorial for potential users rather than a monograph for researchers. The book has three parts: Elementary Techniques; Logic and Sets; Advanced Material.

Download or read it online for free here:

**Download link**

(1.2MB, PDF)

## Similar books

**Curves and Surfaces in Geometric Modeling: Theory and Algorithms**

by

**Jean Gallier**-

**Morgan Kaufmann**

This book offers both a theoretically unifying understanding of polynomial curves and surfaces and an effective approach to implementation that you can bring to bear on your own work -- whether you are a graduate student, scientist, or practitioner.

(

**6534**views)

**An Architecture for Combinator Graph Reduction**

by

**Philip J. Koopman, Jr.**-

**Academic Press**

The results of cache-simulation experiments with an abstract machine for reducing combinator graphs are presented. The abstract machine, called TIGRE, exhibits reduction rates that compare favorably with previously reported techniques.

(

**15935**views)

**Algorithmic Algebra**

by

**Bhubaneswar Mishra**-

**Courant Institute of Mathematical Sciences**

The main purpose of the book is to acquaint advanced undergraduate and graduate students in computer science, engineering and mathematics with the algorithmic ideas in computer algebra so that they could do research in computational algebra.

(

**21741**views)

**Implementing Mathematics with The Nuprl Proof Development System**

by

**R. L. Constable, at al.**-

**Prentice Hall**

The authors offer a tutorial on the new mathematical ideas which underlie their research. Many of the ideas in this book will be accessible to a well-trained undergraduate with a good background in mathematics and computer science.

(

**16158**views)