cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
If `misc` defines constants, you have to have its grammar in scope to see them cleanly (the alternative is having to write `misc$constname`). But if you do that, you also...
HOL supports packaging a built development for reuse on another machine via its `relocbuild` argument to `build` and `Holmake`. However, the packaging and reuse process is a bit fiddly and...
CakeML's `miscTheory` and `preamble` contain many general-purpose theorems and tools that are supposed to be upstreamed to HOL wherever possible. This issue is to do an upstreaming pass. To resolve...
Several people have contacted us asking to have the CakeML semantics in provers other than HOL4. There is an [AFP entry](https://devel.isa-afp.org/entries/CakeML.html) with the CakeML semantics ported to Isabelle/HOL via Lem....
It's common to want the top-level translated functions to not have pre-conditions or side-conditions. The CakeML development indirectly requires this with the top-level CF theorems stated about the final toplevel...
(Explicitly doing work hinted at in #321). The proofs in particular to package up and export would include the compiler correctness proof (at the machine-code level) and the OpenTheory reader...
At present, CakeML’s source code has two word sizes: 8 and 64. This issue is about supporting any word size as if it is primitive type, ie by writing word7...
This code: ```sml fun supervisor x = ( FirstFunc.firstFunc (); SecondFunc.secondFunc () ); ``` Produces this s-expr, which parses fine (with `cake --sexp=true`) ``` (Tdec (Dletrec (0 0 0 0...
Currently, [mlstringTheory](https://github.com/CakeML/cakeml/blob/master/basis/pure/mlstringScript.sml#L13) defines a function `implode` as follows. val implode_def = Define` implode = strlit` which is exactly the same as the (only) constructor `strlit` for the `mlstring` type, which...
Hi, With the following datatype: ```ml datatype 'a misc_app_list = Nil | Append of 'a misc_app_list * 'a misc_app_list | List of 'a list; ``` Here's an example of what...
