| Thread Previous • Date Previous • Date Next • Thread Next |
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?
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.
The plan that I've outlined above is just a starting point. Any feedback and suggestions would be appreciated.
- Larry
| Thread Previous • Date Previous • Date Next • Thread Next |
