The Coq mailing list

[<llee AT jhsph.edu>]

Scheme is a popular dialect of Lisp that posses an elegant syntax and powerful
semantics.

It's development is directed by a steering committee (the Scheme Steering
Committee (http://scheme-reports.org/)) that recently released a document
describing the latest version of the language - R7RS. They are currently
looking for implementations.

I'm starting a project to create an open-source formally verified compiler for
Scheme, and am looking for people who are interested in participating. My
intention is to develop a Coq library that models the new language standard
and to develop a compiler in Scheme that is formally verified using this
model. The model itself should be accessible to Scheme developers so that it
may be used to verify programs written in Scheme. The compiler should
emphasize reliability and correctness to ensure that it can be used in high-
reliability applications.

Anyone interested in participating is welcome. I'm looking to assemble a small
team to get this project off the ground. If you're interested, please email
me.

More information about the project can be found here:
https://launchpad.net/willow-r7rs.

Thanks,
- Larry D. Lee jr. [% user.email %]