Búsqueda avanzada

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.

Palabras Clave:

abstract machine - Big-step machine - compiler verification - Coq - de Bruijn indices - Mini-ML - natural semantics - SECD





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

Descarga el artículo haciendo click aquí.