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},
}
|