# VFAVerified Functional Algorithms

### by Andrew W. Appel

# Introduction

*Software Foundations*series, which presents the mathematical underpinnings of reliable software.

*deductively verified for functional correctness*, that is, you should prove that it behaves correctly on all inputs. That can't be achieved by

*testing*alone, unless there are only a finite number of possible inputs. I say "some software" because many programs, perhaps most programs, don't need to be correct; or we can't even specify what the "correct" behavior would be. But the programs we must rely on—to protect us from malicious inputs sent by hackers, to protect one untrusted program from another, to calculate life-critical values in airplanes or medical devices—are worth writing carefully and then proving correct.

*maintained*, and their proofs must be maintained with them. Therefore, while humans can usually check proofs in mathematics, it takes a computer to check proofs in software engineering.

*programming language*, use the

*proof theory*(or

*program logic*) of that language to state correctness theorems and prove them, and use a

*proof assistant*(or sometimes a

*theorem prover*) to manage the creation of the proof, check the proof, and check the correspondence of the proof to the program.

*Verified Functional Algorithms*. The language is

*Gallina*, the pure functional language embedded in the Coq logic. The proof theory is Coq's Calculus of Inductive Constructions (CiC), the proof assistant is Coq, and the mechanical checker, both for proofs of theorems and correspondence of the theorems to the programs, is the Coq kernel. Programs can then be

*extracted*from Coq to run in ML (Ocaml), Haskell, Lisp, or other functional languages.

*functional algorithms*(as compared to imperative algorithms) can be used only where this factor-of-logN penalty is affordable.

*in Coq*their asymptotic efficiency, but we will reason about it informally (that is, using proofs that mathematicians would call "formal" but proof-assistant users call "informal.") And, in some chapters, we will extract the programs to ML, compile them with the optimizing Ocaml compiler, and measure their performance.

# Prerequisites and practicalities

*Software Foundations*is that it is one hundred percent formalized and machine-checked: the entire text is literally a script for Coq. It is intended to be read alongside an interactive session with Coq. All the details in the text are fully formalized in Coq, and the exercises are designed to be worked using Coq.

## Chapter Dependencies

*Verified Functional Algorithms*, read (and do the exercises in) these chapters of

*Software Foundations Volume I*: Preface, Basics, Induction, Lists, Poly, Tactics, Logic, IndProp, Maps, and perhaps (ProofObjects), (IndPrinciples).

- Sort -> ( Multiset or Selection or Decide )
- SearchTree -> ( ADT or Extraction )
- Perm -> Trie
- Sort -> Selection -> SearchTree -> ADT -> Priqueue -> Binom

## System Requirements

_{2}.

## Exercises

- One star: easy exercises that underscore points in the text
and that, for most readers, should take only a minute or two.
Get in the habit of working these as you reach them.
- Two stars: straightforward exercises (five or ten minutes).
- Three stars: exercises requiring a bit of thought (ten
minutes to half an hour).
- Four and five stars: more difficult exercises (half an hour and up).

*Please do not post solutions to the exercises in any public place*: Software Foundations is widely used both for self-study and for university courses. Having solutions easily available makes it much less useful for courses, which typically have graded homework assignments. The authors especially request that readers not post solutions to the exercises anyplace where they can be found by search engines.

## Downloading the Coq Files

http://www.cs.princeton.edu/~appel/vfa/vfa.tgzIf you are using the notes as part of a class, your professor may give you access to a locally extended version of the files, which you should use instead of the release version.

## Acknowledgment

## For instructors and contributors

*I hereby assign copyright in my past and future contributions to the Software Foundations project to the Author of Record of each volume or component, to be licensed under the same terms as the rest of Software Foundations. I understand that, at present, the Authors of Record are as follows: For Volumes 1 and 2, known until 2016 as "Software Foundations" and from 2016 as (respectively) "Logical Foundations" and "Programming Foundations," the Author of Record is Benjamin Pierce. For Volume 3, "Verified Functional Algorithms", the Author of Record is Andrew W. Appel. For components outside of designated Volumes (e.g., typesetting and grading tools and other software infrastructure), the Author of Record is Benjamin Pierce*.