CakeML / CakeML/cakeml

Update CakeML tutorial to use monadic translator

Open
#697 1 comment 0 reactions 0 assignees View on GitHub
help wanted
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.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.