coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Software Foundations, version 4.0

From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Software Foundations, version 4.0
Date: Mon, 6 Jun 2016 06:58:10 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT hound.seas.upenn.edu
Ironport-phdr: 9a23:3nIv7xEjU+F3VJXZ4Fo1E51GYnF86YWxBRYc798ds5kLTJ75o8qwAkXT6L1XgUPTWs2DsrQf27uQ7fGrAjRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nhqbsqtaIO01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y5WeGgQkBNNAg6Nx1eyZpb8qCD3/KIp0iKCPMDsRr0cUjW5qbpzRRnuzioLKmhqoynslsVsgfcD81qarBtlztuMbQ==

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

[Coq-Club] Software Foundations, version 4.0, Benjamin C. Pierce, 06/06/2016