willow-dev-team team mailing list archive

[AUGER Cédric <sedrikov@xxxxxxxxx>]

Le Sun, 04 May 2014 07:37:24 -0400,
"Larry D. Lee jr" <llee@xxxxxxxxxxxxxxxxxxxx> a écrit :

> Hi Team,
> 
> I've finished recruiting members to the Willow Project, and believe
> that we have enough people on board to begin development. Before we
> begin, however, I would like to take some time to work out the
> general architecture for the project and to identify and assign
> various tasks.
> 
> My original plan for the Willow project is to create a Coq module
> named "Scheme.R7RS". This module will encode the operational
> semantics for R7RS following the naming conventions and model
> developed in Chapter 7 ("Formal Syntax and Semantics") of the R7RS
> report. My plan is to extract this interpreter towards a target
> language such as Scheme and use this extracted interpreter for a
> latter step. This first step can be divided into two tasks. The first
> is to develop a parser to parse R7RS expressions in Coq. The second
> is to draft the operational semantics module. Is anyone interested in
> taking on either task?

I am interested in drafting operational semantics.

> 
> After the Coq module was developed, my intention was to create a 
> compiler, written in R7RS itself. I have not settled on a target 
> language and we probably should. This compiler could then be verified
> as correct using the Coq module, and could be compiled using the
> extracted interpreter. Developing this compiler is a complex task in
> itself and I'd like to know if anyone would be interested in taking
> this on.

We will see once we have an interpreter. I hoped that you had a target
machine in mind before starting the project…

> 
> The plan that I've outlined above is just a starting point. Any
> feedback and suggestions would be appreciated.
> 
> - Larry
>