search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
937 stars 81 forks source link

Support composition of CF-verified functions #291

Open xrchz opened 7 years ago

xrchz commented 7 years ago

This issue is to ensure that function composition (o) is usable in CF-verified programs that inherit the basis library. (I don't know if it means o needs to be translated specially at some point and added into one of the basis library prog scripts, or if an existing translation needs to be properly exposed, or something else.)

xrchz commented 6 years ago

Update: composition is there, but the problem is using it with impure functions. This is a special case of the standard problem with higher-order CF. (For only pure functions, the translator should be used instead.)

As a concrete example, how can we use the CF framework to verify this declaration: val print_int = TextIO.print_string o Int.toString