package coq-mini-compiler

  1. Overview
  2. No Docs
Correctness of a tiny compiler for arithmetic expressions

Install

Dune Dependency

Authors

Maintainers

Sources

v8.6.0.tar.gz
md5=89efeb6a9a6e5b8d8932636568cd2a63

Description

Tutorial correctness proof of a tiny compiler from simple arithmetic expressions (constants, variables and additions) to simple assembly-like code (one accumulator, infinitly many registers and addition)

Dependencies (2)

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

Dev Dependencies

None

Used by

None

Conflicts

None