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. H
    Hugo.Herbelin@inria.fr

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

Tags

keyword: functional programming keyword: Categorical Abstract Machine keyword: compilation keyword: natural semantics category: Computer Science/Semantics and Compilation/Compilation

Published: 07 Dec 2019

Dependencies (2)

  1. coq >= "8.10" & < "8.11~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None