Proving Correctness of a Compiler Using Step-indexed Logical Relations
- Rodríguez, Leonardo
- Pagano, Miguel
- Fridlender, Daniel
Publication date
July 2016
DOI Publisher
The Author(s). Published by Elsevier B.V.Abstract
AbstractIn this paper we prove the correctness of a compiler for a call-by-name language using step-indexed logical relations and biorthogonality. The source language is an extension of the simply typed lambda-calculus with recursion, and the target language is an extension of the Krivine abstract machine. We formalized the proof in the Coq proof assistant
Add to ORKG