Navegación

Búsqueda

Búsqueda avanzada

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):

Handle:

11705/PROLE/2012/001

Descargas:

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

Descarga el artículo haciendo click aquí.