Skip to Main content Skip to Navigation
Master Thesis

Krivine Realizability for Compiler Correctness

Guilhem Jaber 1, 2
2 ASCOLA - Aspect and composition languages
Inria Rennes – Bretagne Atlantique , Département informatique - EMN, LINA - Laboratoire d'Informatique de Nantes 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.
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

https://dumas.ccsd.cnrs.fr/dumas-00530710
Contributor : Co-Responsables Du Mri V. Gouranton Et S. Blazy <>
Submitted on : Friday, October 29, 2010 - 4:46:38 PM
Last modification on : Monday, February 15, 2021 - 10:37:43 AM
Long-term archiving on: : Friday, October 26, 2012 - 12:41:44 PM

Identifiers

  • HAL Id : dumas-00530710, version 1

Citation

Guilhem Jaber. Krivine Realizability for Compiler Correctness. Symbolic Computation [cs.SC]. 2010. ⟨dumas-00530710⟩

Share

Metrics

Record views

304

Files downloads

298