The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Formalizing and implementing verified compilers is a sort of boutique
area that some of the Coq community members are pretty well versed in
(I'm not one of them).

Presumably what you want to do is to model the definition of Scheme
(or whatever) given it's abstract machine formalizations that are (at
this point) folklore.  Then you want to prove the correctness of the
translation in the sense that if you take a program and execute it
using the abstract machine semantics you get an agreement if you
execute the assembly code (or whatever your base is).

One thing that seems suspect is the following: writing the compiler in
Scheme itself doesn't seem trivial.  People usually write the
compilers in Coq so that they can use the facilities of the logic to
argue about the correctness of the compiler.  If you wrote your
compiler in Scheme you'd have to do essentially the same thing, except
a lot more work because you'd have to reason through the embedding of
the semantics.  That seems super nasty.

This is a pretty ambitious open source project, considering that
CakeML is definitely what I'd describe as active research :-)

Kris


On Wed, Apr 23, 2014 at 10:35 AM,  
<llee AT jhsph.edu>
 wrote:
> 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 %]