cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
The translator currently only supports recursion under type constructors for a few hard-coded types `pair`, `option` and `list`. For a minimal example, consider these types: ``` Datatype: container = Container...
This issue is about extending the translator with support for mutually recursive datatypes. Below is a target example, which currently fails due to limitations of the translator's `register_type` function. ```...
This issue is about adding support for the bitmap and code buffers to all of the exporters (except x64, which already has them).
The following operations would be useful additions to the Word{8,64} modules: - `val * : word -> word -> word` - `val / : word -> word -> word` -...
(Feature request) We already have Word64.toInt that treats the word as an unsigned integer. It would be useful to also have a version that treats the word as a signed...
Currently, the floating point semantics of all CakeML ILs just delegates to `machine_ieee`, which uses a @ term to select a NaN to return in cases where that is the...
Currently, the only way to create floating point numbers is to parse them from string. Pretty much the only useful things I can do with these floating point numbers is...
(descoped from #773) Given a potentially hot function, we should not allocate data in the function which is known to be constant. Define a "deep constant" to be a closLang...
This issue will track the progress of adding `open` and `let open` forms to the CakeML syntax and semantics. It is _almolst_ possible to emulate the functionality of `open` using...