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

Sources

v8.10.0.tar.gz
md5=435a68bd17a447f53614a54cc5f304ca

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 Dec 2019

Dependencies (2)

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

Dev Dependencies

None

Used by

None

Conflicts

None