Update CakeML tutorial to use monadic translator
- Dominant language
- Standard ML
- Stars
- 1.2k
- Forks
- 104
- Avg merge
- 2d 21h
- Merged PRs (30d)
- 16
Description
Currently the CakeML tutorial, i.e. the files under [tutorial/solutions](https://github.com/CakeML/cakeml/tree/master/tutorial/solutions) and particularly
[wordfreqProgScript.sml](https://github.com/CakeML/cakeml/blob/master/tutorial/solutions/wordfreqProgScript.sml), is based on CF proofs.
Since the monadic translator, which is described in [Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions](https://cakeml.org/ijcar18.pdf), could produce the same program in a nicer way, I think the tutorial should be ported to use the monadic translator.
One can take inspiration from [existing examples that use the monadic translator](https://github.com/CakeML/cakeml/tree/master/translator/monadic/examples).
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.