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.
Type de document :
Rapport
[Research Report] RR-2536, INRIA. 1995
Liste complète des métadonnées

https://hal.inria.fr/inria-00074142
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:36:34
Dernière modification le : samedi 17 septembre 2016 - 01:35:47
Document(s) archivé(s) le : dimanche 4 avril 2010 - 22:12:52

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

140

Téléchargements de fichiers

364