Krivine realizability for compiler correctness

Guilhem Jaber 1 Nicolas Tabareau 2, 3
3 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
Abstract : We propose a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple functional language to SECD machine code. Our result is quite independent from the source language as it uses Krivine's realizability to give a denotational semantics to SECD machine code using only the type system of the source language. We use realizability to prove the correctness of both a call-by-name (CBN) and a call-by-value (CBV) compiler with the same notion of orthogonality. We abstract over the notion of observation (e.g. divergence or termination) and derive an operational correctness result that relates the reduction of a term with the execution of its compiled SECD machine code.
Type de document :
Pré-publication, Document de travail
2010
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-00475210
Contributeur : <>
Soumis le : mercredi 21 avril 2010 - 14:36:39
Dernière modification le : vendredi 6 février 2015 - 12:26:49
Document(s) archivé(s) le : lundi 22 octobre 2012 - 15:15:28

Fichier

lola-1.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00475210, version 1
  • Mot de passe :

Collections

Citation

Guilhem Jaber, Nicolas Tabareau. Krivine realizability for compiler correctness. 2010. 〈hal-00475210v1〉

Partager

Métriques

Consultations de la notice

7

Téléchargements de fichiers

34