A Generic Framework for Verified Compilers

Martin Desharnais 🌐

February 10, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

History

July 10, 2024
Generalized the definition of bisimulation to have distinct orderings for forward and backward simulations. Added lemmas for composition of forward simulations and bisimulations.
November 27, 2023
Added a generic, framework-independent lemma to lift a simulation to a bisimulation.

Topics

Session VeriComp

Used by

Cite

× 
@article{VeriComp-AFP,
  author  = {Martin Desharnais},
  title   = {A Generic Framework for Verified Compilers},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/VeriComp.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: