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.6.0

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