Búsqueda avanzada

Resultados de búsqueda para natural semantics

A Correct Compiler from Mini-ML to a Big-Step Machine Verified Using Natural Semantics in Coq (Trabajo en progreso)

This work has the objective to present a simple, clear and intuitive framework for compilers verification of functional languages in the proof assistant Coq, that, as a final product, can obtain a standalone verified compiler capable of being used in real life. With this in mind, we propose to use natural semantics as unifying framework, that is to say, to use this formalism to define each of the compiler’s components in order to perform this task. To show this method, we present a correct compiler of the small functional language with call by value Mini-ML, formalized in Coq. As a result of following this approach, we introduce a new big-step  machine inspired by Landin’s SECD and Leroy’s Modern SECD as target machine. To the best of the authors’ knowledge, this is the first correct compiler that is verified by using natural semantics as unifying framework in Coq from which we can obtain a verified compiler capable of being used in real life.

Autores: Ángel Zúñiga / Gemma Bel-Enguix / 
Palabras Clave: abstract machine - Big-step machine - compiler verification - Coq - de Bruijn indices - Mini-ML - natural semantics - SECD

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

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.

Autores: Lidia Sánchez-Gil / Mercedes Hidalgo-Herrero / Yolanda Ortega-Mallén / 
Palabras Clave: Coq - Formalization - lazy evaluation - locally nameless representation - natural semantics - proof assistant

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada