package coq-mini-compiler

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

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. J
    Jean-Christophe Filliâtre <>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=27b1414ce51c9cfe014d5777e9d47b2e

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)

Tags

keyword:compilation keyword:correctness keyword:arithmetic category:Computer Science/Semantics and Compilation/Compilation date:2003

Published: 07 Jun 2016

Dependencies (2)

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

Dev Dependencies

None

Used by

None

Conflicts

None