coq-miniml

Correctness of the compilation of Mini-ML into the Categorical Abstract Machine. A formalisation of Mini-ML and of the Categorical Abstract Machine (C.A.M) in natural semantics. It also contains the definition of the translation from Mini-ML to the CAM and the proof that this translation is correct

opam install coq-miniml.8.5.0
homepage
https://github.com/coq-contribs/miniml
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/miniml/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/miniml/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-miniml/coq-miniml.8.5.0