A Correct Compiler from Mini-ML to a Big-Step Machine Verified Using Natural Semantics in Coq





Publicado en

Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018)

Licencia Creative Commons


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.


Acerca de Zúñiga, Ángel

Palabras clave

Abstract Machine, Big-step Machine, Compiler Verification, Coq, De Bruijn Indices, Mini-ML, Natural Semantics, SECD
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX