Coinductive Natural Semantics for Compiler Verification in Coq

Angel Zúñiga and Gemma Bel-Enguix
Additional contact information
Angel Zúñiga: Posgrado en Ciencia e Ingeniería de la Computación, Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, Universidad Nacional Autónoma de México, Mexico City 04510, Mexico
Gemma Bel-Enguix: Instituto de Ingeniería, Universidad Nacional Autónoma de México, Mexico City 04510, Mexico

Mathematics, 2020, vol. 8, issue 9, 1-55

Abstract: (Coinductive) natural semantics is presented as a unifying framework for the verification of total correctness of compilers in Coq (with the feature that a verified compiler can be obtained). In this way, we have a simple, easy, and intuitive framework; to carry out the verification of a compiler, using a proof assistant in which both cases are considered: terminating and non-terminating computations (total correctness).

Keywords: natural semantics; big-step semantics; coinduction; compiler verification; total correctness; Mini-ML; SECD machine; Coq proof assistant (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2020
References: View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
https://www.mdpi.com/2227-7390/8/9/1573/pdf (application/pdf)
https://www.mdpi.com/2227-7390/8/9/1573/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:8:y:2020:i:9:p:1573-:d:412629

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().