Autor:
Bel-Enguix, Gemma

Cargando...
Foto de perfil

E-mails conocidos

gbele@iingen.unam.mx

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Bel-Enguix

Nombre de pila

Gemma

Nombre

Nombres alternativos

Afiliaciones conocidas

UNAM, Mexico

Páginas web conocidas

Página completa del ítem
Notificar un error en este autor

Resultados de la búsqueda

Mostrando 1 - 1 de 1
  • Artículo
    A Correct Compiler from Mini-ML to a Big-Step Machine Verified Using Natural Semantics in Coq
    Zúñiga, Ángel; Bel-Enguix, Gemma. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
    This paper presents a correct compiler of a small functional language, Mini-ML, formalized in Coq. The literature of functional compiler verification in proof assistants usually reports the use of ad hoc formalizations. This work emphasized the use of natural semantics as uniform and unifying framework for this task. As a result of following this approach, a new big-step semantics machine with call by value is introduced, inspired by the SECD of Landin and the MSECD of Leroy. Since this machine uses de Bruijn indices, as first step is giving a (correct verified) translation from named Mini-ML to de Bruijn notation Mini-ML in the natural semantics setting. To the best of the author's knowledge, this is the first mechanization of a correct compiler of a functional language, using natural semantics as verifying framework in a proof assistant, such as, a working compiler capable to be used in real life can be obtained from it.