cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
See https://smlfamily.github.io/Basis/char.html#SIG:CHAR.toString:VAL and https://smlfamily.github.io/Basis/string.html#SIG:STRING.toString:VAL
The labels are now removed from the Pancake syntax, but there are still some residual syntactic redundancy that we should clean up. Namely, ``` Datatype: word_lab = Word ('a word)...
This issue is about implementing a resizable stack for CakeML. Currently CakeML's stack size is determined at initial runtime.
The lack of variable-length shifts has been a blocker for a number of optimisations and improvements. This issue is about adding variable-length shifts to [asm](https://github.com/CakeML/cakeml/blob/master/compiler/encoders/asm/asmScript.sml) and supporting them in all...
CakeML has vectors (immutable) and arrays (mutable). Both have O(1) access and update. This issue is about implementing [persistent arrays](https://en.wikipedia.org/wiki/Persistent_array) in CakeML. If used carefully, persistent arrays have similar performance...
Currently, `Vector.tabluate` is a straightforward translation of the following function from `mlvectorScript.sml`: val tabulate_def = Define` tabulate n f = Vector (GENLIST f n)`; For large `n`, this is a...
We should try to use the translator's brittle "treat `string` as if it is `mlstring`" feature much less. This issue is about replacing all occurrences of `string` in [semantics/astScript.sml](https://github.com/CakeML/cakeml/blob/master/semantics/astScript.sml) with...
Isabelle's afp has a version of the CakeML semantics but that's based on old lem semantics. This issue is about creating a updated version of the semantics. It should be...
This issue is about adding a new subfolder in examples/ to manage proof checker implementations, at least those working over Boolean-valued variables. In particular, there are many routines and definitions...
This issue is about adding support for record selector syntax for CakeML tuples. i.e. ```#1 (a,b)```. The main difficulty in implementing it is such that if a fixed tuple type...