[ecoop-info] Software Foundations, version 4.0

[Benjamin C. Pierce]

I’m delighted to announce a new edition of Software Foundations, an electronic textbook on the theory of programming languages covering functional programming, constructive logic, Hoare Logic, type systems, and formal verification using Coq.  The whole book — definitions, theorems, proofs, and extensive exercises — is machine checked using Coq.

Previous editions have been widely used in both graduate and upper-level undergraduate courses as well as for self-study.  The new edition features a significant rearrangement and clarification of the central chapters on logic in Coq; in particular, the concept of “proof object” and the Curry-Howard isomorphism have been rewritten and moved off the critical path, permitting a more flexible choice of material in courses.  Plus numerous smaller improvements throughout.

Software Foundations can be downloaded from http://www.cis.upenn.edu/~bcpierce/sf <http://www.cis.upenn.edu/~bcpierce/sf>