Lambda the Ultimate

This announcement has been made in various places, including comp.lang.scheme:

March 7, 2006

Since the last report of the Steering Committee, a number of important changes have taken place.

First, Marc Feeley and Manuel Serrano have resigned from the Editors Committee. We have accepted their resignations with regret, and with gratitude for the efforts they have expended to produce a revised Scheme standard.

In light of these changes, the Steering Committee has amended the Charter to:

(a) change the number of Editors from seven to five.

(b) replace the office of Editor-in-Chief by a Chair and a Project Editor. The Chair is responsible for organizing meetings and other activities and ensuring that the process makes progress in an orderly fashion. The Project Editor is responsible for producing standardization documents.

The five editors have chosen their Chair and Project Editor. They are:

Chair: Kent Dybvig
Project Editor: Mike Sperber

The Editors Committee has now produced a progress report, which is available at schemers.org. In it they state their intention to deliver to the Steering Committee a complete draft R6RS by September 1, 2006.

The Steering Committee looks forward to receiving their draft.

Alternate links to the Editors' Progress Report:

http://www.cs.indiana.edu/~dyb/r6rs/status.pdf
http://www.cs.indiana.edu/~dyb/r6rs/status.html

---The Scheme Language Steering Committee:
Alan Bawden
Guy Steele
Mitch Wand

Via the plt-scheme mailing list:

We are pleased to announce the first public release [beta 7] of ACL2
in DrScheme, a combination of the ACL2 theorem prover system with the
DrScheme programming environment. The objective of this project is
to provide a development environment for ACL2 suitable for novice
users as well as enhancements of ACL2 that are attractive for the
typical undergraduate student (graphics, interactive games, sound).

There's a tutorial with screenshots and some examples on the ACL2 in DrScheme web page.

I'm always happy to see reasoning about programs introduced at the undergraduate level. I wonder what the LtU community would do with a tool like this. What cool things would you teach with a beginner's theorem prover?