Un compilador correcto verificado de mini-ml a la máquina SECD en Coq - Zúñiga Chávez, Ángel Francisco (MX, 2016)