The Little Prover by Daniel P. FriedmanThe Little Prover by Daniel P. Friedman

The Little Prover

byDaniel P. Friedman, Carl EastlundDrawings byDuane Bibby

Paperback | July 10, 2015

Pricing and Purchase Info

$46.09 online 
$52.00 list price save 11%
Earn 230 plum® points

Prices and offers may vary in store


In stock online

Ships free on orders over $25

Not available in stores


An introduction to writing proofs about computer programs, written in an accessible question-and-answer style, complete with step-by-step examples and a simple proof assistant.

The Little Prover introduces inductive proofs as a way to determine facts about computer programs. It is written in an approachable, engaging style of question-and-answer, with the characteristic humor of The Little Schemer (fourth edition, MIT Press). Sometimes the best way to learn something is to sit down and do it; the book takes readers through step-by-step examples showing how to write inductive proofs. The Little Prover assumes only knowledge of recursive programs and lists (as presented in the first three chapters of The Little Schemer) and uses only a few terms beyond what novice programmers already know. The book comes with a simple proof assistant to help readers work through the book and complete solutions to every example.

Daniel P. Friedman is Professor of Computer Science at Indiana University and coauthor of The Little Schemer (fourth edition), The Reasoned Schemer, The Seasoned Schemer, and Essentials of Programming Languages (third edition), all published by the MIT Press. Carl Eastlund is a software engineer at Jane Street Capital in New York Ci...
Title:The Little ProverFormat:PaperbackProduct dimensions:248 pages, 9 × 7 × 0.56 inShipping dimensions:9 × 7 × 0.56 inPublished:July 10, 2015Publisher:The MIT PressLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:0262527952

ISBN - 13:9780262527958


Editorial Reviews

Friedman and Eastlund's The Little Prover is a gentle introduction to the nuts and bolts of formal proofs about programs. Following on from The Little Schemer, it is an excellent guide for both thoughtful functional programmers wondering what it really means to know that a program is correct and do-it-yourselfers who want a taste of how proof assistants like ACL2 do their work. Bring your sense of humor and your thinking cap!-Benjamin C. Pierce, Henry Salvatori Professor of Computer and Information Science, University of Pennsylvania