Section outline
-
Presentation of an abstract machine close to assembly code.
It will be endowed with an operational semantics.
The main purpose is to give you an idea of how to argue about the correctness of the implementation of a compiler for a given programming language.
We will see:
- how to define an operational semantics for an abstract machine: a machine with an evaluation stack
- how to specify a code generator for such a machine (translation functions on the syntax of While language)
- how to use the source and target language semantics to prove that the code generation is correct