Contribution: MiniCompiler
Correctness of a tiny compiler for arithmetic expressions
Authors
- Jean-Christophe Filliâtre
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)
Keywords
compilation, correctness, arithmetic