A formalization in Coq of Launchbury~s natural semantics for lazy evaluation

Resumen:

We are working on the implementation of Launchbury~s semantics for lazy evaluation in the proof assistant Coq. We use a locally nameless representation where names are reserved for free variables, while bound variable names are replaced by indices. This avoids the need of -conversion and Barendregt~s variable convention, and facilitates the formalization in Coq. Simultaneous recursive local declarations in the calculus require the management of multibinders and the use of mutually inductive types.

Palabras Clave:

Coq - Formalization - lazy evaluation - locally nameless representation - natural semantics - proof assistant

Autor(es):

• Lidia Sánchez-Gil {lidiasg@mat.ucm.es}
  Dpt. Sistemas Informáticos y Computación, Facultad de CC. Matemáticas, Universidad Complutense de Madrid, Spain
  
• Mercedes Hidalgo-Herrero {mhidalgo@edu.ucm.es}
  Dpt. Didáctica de las Matemáticas, Facultad de Educación, Universidad Complutense de Madrid, Spain
  
• Yolanda Ortega-Mallén {yolanda@sip.ucm.es}
  Dpt. Sistemas Informáticos y Computación, Facultad de CC. Matemáticas, Universidad Complutense de Madrid, Spain
  

Handle:

Descargas:

Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex