myreen
myreen
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. ```...
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...
[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...
Arthur Charguéraud has developed a new version of CFML based on weakest preconditions. Here are a few URLs: - [his course on separation logic ](http://www.chargueraud.org/teach/verif/) - [his construction of wpgen](http://www.chargueraud.org/teach/verif/slf/LibSepReference.html)...
Currently stackLang programs write a number onto the stack at each function call. The number is an index into the bitmaps (used by the GC if it is called). An...
Currently, [the compiler is allowed to](https://github.com/CakeML/cakeml/blob/master/compiler/proofs/compilerProofScript.sml#L125) return `Failure CompileError` for any input program. At present, these compiler errors can only occur when a code label is too far from the...
We want to compile HOL functions that essentially only operate over a memory modelling function and word types to wordLang (phase 1) and from there compile it to concrete machine...