The Coq mailing list

["Andrew W. Appel" <appel AT CS.Princeton.EDU>]

I am pleased to announce the beta release of Verified Functional Algorithms,

a new volume in the Software Foundations series.

http://www.cs.princeton.edu/~appel/vfa/

Do you teach with Software Foundations?  Did you ever want to teach

a week or two (or 6) about applications of Coq to functional programming?

Did you ever want to tell your students that there are applications of Coq

other  than reasoning about the operational semantics of programming languages?

Now you can use VFA, the whole thing or just a chapter or two,

after just the first few chapters of Software Foundations.

Software Foundations is the successful and widely used interactive-in-Coq

textbook by Benjamin Pierce et al.  Starting with the its next release (5.0,

expected in early 2017), Software Foundations will be divided into these volumes:

Volume 1:  Logical Foundations, by Benjamin Pierce et al.

Chapters Preface, Basics, Induction, Lists, Poly, Tactics, Logic, IndProp,

Maps, ProofObjects, IndPrinciples.

Volume 2:  Programming Language Foundations, by Benjamin Pierce et al.

Chapters Rel, Imp, ImpParser, ImpCEvalFun, Extraction, Equiv, Hoare, Hoare2,

HoareAsLogic, Smallstep, Auto, Types, Stlc, StlcProp, MoreStlc, Sub, Typechecking,

Records, References, RecordSub, Norm, LibTactics, UseTactics, UseAuto, PE,

Postscript, Bib.

And now, the new,

Volume 3: Verified Functional Algorithms, by Andrew W. Appel

Chapters VFA, Perm, Sort, Multiset, Selection, SearchTree, ADT, Extraction,

Redblack, Trie, Priqueue, Binom, Decide, Color.

The material in Volume 3 depends only on the Volume 1 material; you

can use VFA as an alternative to Programming Language Foundations, or

you can do some of each. Students learn how to specify and verify sorting

algorithms, binary search trees, balanced binary search trees, and priority queues.

Encapsulation of abstract data types is covered, using Modules and 

(a very limited use of) dependent types.

The textbook covers issues in specification methods in their own right:

How do you know you have the right specification?

Should sorting be specified using permutations or multisets?

Tactic automation is covered, a little bit, as necessary: the correctness proofs

for red-black trees have hundreds of cases, easily dispatched by a disciplined use of Ltac.

If you wish to teach using Verified Functional Algorithms during the coming

academic year, read the beta release (and try the exercises!), and send me mail.

Sincerely,

Andrew Appel

  [VFA is a component of the Education mission of the DeepSpec expedition.]