package coq-miniml

  1. Overview
  2. No Docs
Correctness of the compilation of Mini-ML into the Categorical Abstract Machine

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. S
    Samuel Boutin <>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=ad1936dc8998fe3bba52b15abd7deea4

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

Tags

keyword:functional programming keyword:categorical abstract machine keyword:compilation keyword:natural semantics category:Computer Science/Semantics and Compilation/Compilation

Published: 07 Jun 2016

Dependencies (2)

  1. coq >= "8.5" & < "8.6~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None