# Theory Expr_Compiler

section ‹Correctness of a simple expression compiler›
theory Expr_Compiler
imports Main
begin
text ‹
This is a (rather trivial) example of program verification. We model a
compiler for translating expressions to stack machine instructions, and
prove its correctness wrt.\ some evaluation semantics.
›
subsection ‹Binary operations›
text ‹
Binary operations are just functions over some type of values. This is both
for abstract syntax and semantics, i.e.\ we use a ``shallow embedding''
here.
›
type_synonym 'val binop = "'val ⇒ 'val ⇒ 'val"
subsection ‹Expressions›
text ‹
The language of expressions is defined as an inductive type, consisting of
variables, constants, and binary operations on expressions.
›