Coinductive Natural Semantics for Compiler Verification in Coq

Coinductive Natural Semantics for Compiler Verification in Coq

(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, u...

Full description

Bibliographic Details
Main Authors: Angel Zúñiga, Gemma Bel-Enguix
Format: Article
Language:English
Published: MDPI AG 2020-09-01
Series:Mathematics
Subjects:
natural semantics
big-step semantics
coinduction
compiler verification
total correctness
Mini-ML
Online Access:https://www.mdpi.com/2227-7390/8/9/1573
id doaj-5d0a57478719465e8a4a104edc2b16d5
record_format Article
spelling doaj-5d0a57478719465e8a4a104edc2b16d52020-11-25T03:06:07ZengMDPI AGMathematics2227-73902020-09-0181573157310.3390/math8091573Coinductive Natural Semantics for Compiler Verification in CoqAngel Zúñiga0Gemma Bel-Enguix1Posgrado 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, MexicoInstituto de Ingeniería, Universidad Nacional Autónoma de México, Mexico City 04510, Mexico(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).https://www.mdpi.com/2227-7390/8/9/1573natural semanticsbig-step semanticscoinductioncompiler verificationtotal correctnessMini-ML
collection DOAJ
language English
format Article
sources DOAJ
author Angel Zúñiga
Gemma Bel-Enguix
spellingShingle Angel Zúñiga
Gemma Bel-Enguix
Coinductive Natural Semantics for Compiler Verification in Coq
Mathematics
natural semantics
big-step semantics
coinduction
compiler verification
total correctness
Mini-ML
author_facet Angel Zúñiga
Gemma Bel-Enguix
author_sort Angel Zúñiga
title Coinductive Natural Semantics for Compiler Verification in Coq
title_short Coinductive Natural Semantics for Compiler Verification in Coq
title_full Coinductive Natural Semantics for Compiler Verification in Coq
title_fullStr Coinductive Natural Semantics for Compiler Verification in Coq
title_full_unstemmed Coinductive Natural Semantics for Compiler Verification in Coq
title_sort coinductive natural semantics for compiler verification in coq
publisher MDPI AG
series Mathematics
issn 2227-7390
publishDate 2020-09-01
description (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).
topic natural semantics
big-step semantics
coinduction
compiler verification
total correctness
Mini-ML
url https://www.mdpi.com/2227-7390/8/9/1573
work_keys_str_mv AT angelzuniga coinductivenaturalsemanticsforcompilerverificationincoq
AT gemmabelenguix coinductivenaturalsemanticsforcompilerverificationincoq
_version_ 1724675211032264704

Similar Items