package coq-miniml
Correctness of the compilation of Mini-ML into the Categorical Abstract Machine
Install
Dune Dependency
Authors
Maintainers
Sources
v8.10.0.tar.gz
md5=df00ed94ed18950b75878fd60c827e5c
Description
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
On This Page