Resultados de búsqueda para natural semantics

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.

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.