Bienvenidos a la Iberoteca del mundo libre.
Todas las categorías Ciencias naturales y matemáticas Filosofía y psicología Geografía y historia Religión Tecnología (Ciencias aplicadas) Ciencias sociales Generalidades Las artes Lenguas Literatura y retórica Sin categoría
  2. Documentos
  3. Proving compiler correctness using step-indexed logical relations
Artículos

Proving compiler correctness using step-indexed logical relations

Editorial: Elsevier
 Licencia: Creative Commons (by-nc-nd)
 Autor(es): Rodríguez, Leonardo; [et al.]

In 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.
[Córdoba: 2016]

1.00 €

    Esta combinación no existe.

    Compartir:
    Esta es una vista previa de los documentos vistos recientemente por el usuario.
    Una vez que el usuario haya visto al menos un documento, este fragmento será visible.
    Documentos vistos recientemente