package coq-mini-compiler

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

Install

Dune Dependency

Authors

Maintainers

Sources

v8.9.0.tar.gz
md5=f5679f730d174e15fa5d5396286c3b43

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.9" & < "8.10~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None