cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
This issue proposes adding the following forms to the CakeML syntax and semantics: - Structure abbreviations: `structure S = SuperLongStructName` - Exception abbreviations: `exception E = AnotherException`
Maybe in the commandline module?
Some identifiers that are within lexical scope don't appear in the output of ./cake --types. It's possible that some things will always be missing with the current approach (based on...
If you pass incorrect command line arguments to the CakeML compiler (e.g., misspelled or incorrect format) it silently ignores them. This can lead to surprising or confusing behaviour. The compiler...
The translator mangles the names of functions and type constructors to fit with the CakeML grammar. This mangling can produce non-distinct constructor names, which makes the translator fail. This issue...
At present, functions in WordLang always return one value (of type `word_loc`). This PR is about making it possible to return multiple values (of type `word_loc`) on each function return....
Functions frequently return values as tuples. At present, returning a tuple in CakeML will always produce heap allocation, which is pointless in cases where the caller immediately pattern matches on...
This should involve modify unverified/reg_alloc/reg_alloc.sml (and files that use it) to print the relevant names instead of the function index. Suggested by @myreen
[Deflate](https://en.wikipedia.org/wiki/DEFLATE) is a lossless data compression file format that [zip](https://en.wikipedia.org/wiki/ZIP_(file_format)) and [gzip](https://en.wikipedia.org/wiki/Gzip) are based on. The [deflate algorithm](https://tools.ietf.org/html/rfc1951) would be a nice formalisation and verification exercise in HOL. The result...
It would be nice to have verified implementations of transcendentals (sin, cos, etc) in CakeML. Prior work has been done by John Harrison in his thesis (implementation of CORDIC) and...
