Proving Correctness of the Translation from Mini-ML to the CAM with the Coq Proof Development System
Samuel Boutin, 78 - Rocquencourt (France). Unite de Recherche de Rocquencourt Institut National de Recherche en Informatique et en Automatique (INRIA) · 1995
In this article we show how we proved correctness of the translation from a small applicative language with recursive definitions (Mini-ML) to the Categorical abstract machine (CAM) using the Coq system. Our aim was to mechanise the proof of J. Despeyroux [10]. Like her, we use natural semantics to axiomatise the semantics of our languages. The axiomatisations of inferences systems and of the languages is nicely performed by the mechanism of inductive definitions in the Coq system. Unfortunately both the source and the target semantics involve nested structures that cannot be formalised inductively. We have overcome this problem by making some slight modifications of both the source and target semantics and show how the changes in the source and target semantics are related. For the remaining tranlation we explain how we can use the Coq system to formalize non-terminating programs and incorrect programs, objects that are impossible to explain with only the formalism of natural semantic...