<div dir="ltr">Hi,<div><br></div><div>CakeML is really a great project in which I expect myself to learn almost everything about programming languages (and HOL theorem prover).</div><div><br></div><div>I see the whole work consists of many small modules (as HOL theories) and also depends on HOL's example theories "formal-language" and "l3-machine-code"). I think most of these modules must be general utilities, while the rest of them concern about the CakeML language itself.</div><div><br></div><div>Here is my question: if I want to build at least an interpreter for a toy (not even turing complete) programming language which currently can be seen as a strict sub-set of CakeML (but later I may add object-oriented features to it), and if I want to benefit from existing framework and code of CakeML, *which modules should I look into*, to achieve the following goals:</div><div><br></div><div>1. define the grammar for this language, and get ASTs from any input as mini programs of the toy language.</div><div>2. writing code to do some basic semantic analysis (e.g. type checking, detection of undefined/uninitialized variables).</div><div>3. static analysis: taking a mini program as input, output a theorem saying something like "this program is semantically correct".</div><div>4. actually "run" any mini program in HOL interactive environment.</div><div><br></div><div>Above plan could be one of my exam project (in which other students use Java and ANTLR to do the same thing). I hope in this way I could deeply understand the design and structure of CakeML better, maybe one day I can also make some useful contributions.</div><div><br></div><div>Best Regards,</div><div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>Chun Tian (binghe)<br></div><div>University of Bologna (Italy)</div><div><br></div></div></div></div></div>
</div></div>