# Preface

# Welcome

- Write your program in an expressive language with a good proof theory (the Gallina language embedded in Coq's logic).
- Prove it correct in Coq.
- Compile it with an optimizing ML compiler.

*efficient*, you'll want to implement sophisticated data structures and algorithms. Since Gallina is a

*purely functional*language, it helps to have purely functional algorithms.

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

*Software Foundations Volume 1*(Logical Foundations), but does not depend on Volume 2. The exposition here is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers.

*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.

# Practicalities

## 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 Extract
- Perm -> Trie
- Sort -> Selection -> SearchTree -> ADT -> Priqueue -> Binom

## System Requirements

## 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

## Lecture Videos

## For Instructors and Contributors

*Logical Foundations*for instructions.