Skip to Main content Skip to Navigation
Reports

Proving Correctness of the Translation from Mini-ML to the CAM with the Coq Proof Development System

Abstract : In this report 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 mechanize the proof of J. Despeyroux \cite{Des}. Like her, we use natural semantics to axiomatise the semantics of our languages. We have only partially mecanised the proof. The semantics of the source and target languages use rational trees in their definition and at this stage the Coq system is inefficient in axiomatising such structures. We propose a presentation of the correctness proof to isolate this difficulty.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074142
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:36:34 PM
Last modification on : Friday, May 25, 2018 - 12:02:05 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:12:52 PM

Identifiers

  • HAL Id : inria-00074142, version 1

Collections

Citation

Samuel Boutin. Proving Correctness of the Translation from Mini-ML to the CAM with the Coq Proof Development System. [Research Report] RR-2536, INRIA. 1995. ⟨inria-00074142⟩

Share

Metrics

Record views

210

Files downloads

448