Coinductive Natural Semantics for Compiler Verification in Coq

Abstract

(Coinductive) natural semantics is presented as a unifying framework for the verification of total correctness of compilers in Coq (with the feature that a verified compiler can be obtained). In this way, we have a simple, easy, and intuitive framework; to carry out the verification of a compiler, using a proof assistant in which both cases are considered: terminating and non-terminating computations (total correctness).

Keywords

• natural semantics
• big-step semantics
• coinduction
• compiler verification
• total correctness
• Mini-ML