Re: [Scheme-reports] Looking for collaborators to develop a formally verified implementation for R7RS (small) using Coq.

["Perry E. Metzger" <perry@x>]

On Tue, 22 Apr 2014 10:10:43 -0400 John Cowan
<cowan@x> wrote:
> Larry Lee scripsit:
> 
> > I'm looking to develop an open-source implementation for R7RS
> > that is formally verified. The implementation will be formally
> > verified using Coq (http://coq.inria.fr/) and will focus
> > initially on the small version of the language. If you are
> > interested in assisting with the project, please let me know.
> 
> I can't help with this directly, but I think it has all kinds of
> win. What do you intend to use as the implementation language, or
> is that still open?
> 

Generally, if one does formal verification in Coq, one implements in
Coq itself, and extracts to another language (Haskell, ML, and Scheme
being among the targets Coq supports, although in general OCaml
extraction is the best supported.)

I find the idea of this being done very appealing. I will note
that there isn't a formal semantics currently in existence for R7RS,
but that this project would, by its very nature, create such a
semantics which could be published as a supplement to the existing
report.

-- 
Perry E. Metzger		perry@x

_______________________________________________
Scheme-reports mailing list
Scheme-reports@x
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports