A Generic Framework for Verified Compilers

Title:	A Generic Framework for Verified Compilers
Author:	Martin Desharnais
Submission date:	2020-02-10
Abstract:	This is a generic framework for formalizing compiler transformations. It leverages Isabelle/HOL’s locales to abstract over concrete languages and transformations. It states common definitions for language semantics, program behaviours, forward and backward simulations, and compilers. We provide generic operations, such as simulation and compiler composition, and prove general (partial) correctness theorems, resulting in reusable proof components.
BibTeX:	@article{VeriComp-AFP, author = {Martin Desharnais}, title = {A Generic Framework for Verified Compilers}, journal = {Archive of Formal Proofs}, month = feb, year = 2020, note = {\url{http://isa-afp.org/entries/VeriComp.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.