The Little Prover

The Little Prover

The Little Prover

The Little Prover

Paperback(New Edition)

$40.00 
  • SHIP THIS ITEM
    Temporarily Out of Stock Online
  • PICK UP IN STORE
    Check Availability at Nearby Stores

Related collections and offers


Overview

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.


Product Details

ISBN-13: 9780262527958
Publisher: MIT Press
Publication date: 07/10/2015
Series: The MIT Press
Edition description: New Edition
Pages: 248
Product dimensions: 6.90(w) x 8.90(h) x 2.30(d)
Age Range: 18 Years

About the Author

Daniel P. Friedman is Professor of Computer Science in the School of Informatics, Computing, and Engineering at Indiana University and is the author of many books published by the MIT Press, including The Little Schemer and The Seasoned Schemer (with Matthias Felleisen); The Little Prover (with Carl Eastlund); and The Reasoned Schemer (with William E. Byrd, Oleg Kiselyov, and Jason Hemann).

Carl Eastlund is a software engineer at Jane Street Capital in New York City.

Matthias Felleisen is Trustee Professor in the College of Computer Science at Northeastern University.

Table of Contents

Foreword ix

Preface xi

1 Old Games, New Rules 2 (Examples 181)

2 Even Older Games 14 (Examples 182)

3 What's in a Name? 32 (Proofs 183)

4 Part of This Total Breakfast 42 (Proofs 184)

5 Think It Over, and Over, and Over 58 (Proofs 185)

6 Think It Through 76 (Proofs 187)

7 Oh My, Stars! 88 (Proofs 188)

8 Learning the Rules 106 (Proofs 192)

9 Changing the Rules 114 (Proofs 193)

10 The Stars Are Aligned 138 (Proofs 196)

A Recess 164

B The Proof of the Pudding 180

C The Little Assistant 202

D Restless for More? 216

Afterword 221

Index 222

What People are Saying About This

Shriram Krishnamurthi

Computational theorem proving is so useful, effective, and important that its advocates present it in economic terms: about preventing costly errors in software and protocols. What gets lost is just how much fun it can be. Friedman and Eastlund, two jolly characters, eschew talk of bugs and bombs, and strip it to its essence as only a Little book can. Want proof? Look inside!

Endorsement

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

From the Publisher

Computational theorem proving is so useful, effective, and important that its advocates present it in economic terms: about preventing costly errors in software and protocols. What gets lost is just how much fun it can be. Friedman and Eastlund, two jolly characters, eschew talk of bugs and bombs, and strip it to its essence as only a Little book can. Want proof? Look inside!

Shriram Krishnamurthi, Professor of Computer Science, Brown University

What can you learn about a program without actually running it? What can you know by reading the code? In the grand tradition of The Little LISPer and The Little Schemer, Dan Friedman and Carl Eastlund elegantly present small programs that contain big ideas, but now also show how to prove claims about their behavior. The question-and-answer format makes it surprisingly easy to learn and master inductive proof techniques—it's like eating peanuts! Don't overlook the concise and elegant code for the J-Bob proof assistant itself, tucked in the back. The Little Prover is a marvelous introduction to the program proof techniques used in such tools as ACL2, Isabelle, and Coq.

Guy L. Steele Jr., Software Architect, Oracle Labs, coinventor of the Scheme language, and coauthor of Common LISP: The Language

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

Guy L. Steele Jr.

What can you learn about a program without actually running it? What can you know by reading the code? In the grand tradition of The Little LISPer and The Little Schemer, Dan Friedman and Carl Eastlund elegantly present small programs that contain big ideas, but now also show how to prove claims about their behavior. The question-and-answer format makes it surprisingly easy to learn and master inductive proof techniques—it's like eating peanuts! Don't overlook the concise and elegant code for the J-Bob proof assistant itself, tucked in the back. The Little Prover is a marvelous introduction to the program proof techniques used in such tools as ACL2, Isabelle, and Coq.

Benjamin C. Pierce

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!

From the B&N Reads Blog

Customer Reviews