Definition of CakeML's observational semantics, in particular traces of calls over the Foreign-Function Interface (FFI).
ffiScript.sml: Definition of the FFI type
simpleIOScript.sml: A simple instantiation of the ffi type.
| Name | Name | Last commit date | ||
|---|---|---|---|---|
parent directory.. | ||||
Definition of CakeML's observational semantics, in particular traces of calls over the Foreign-Function Interface (FFI).
ffiScript.sml: Definition of the FFI type
simpleIOScript.sml: A simple instantiation of the ffi type.