### 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

### Topics

- Computer science/Programming languages/Compiling

### Session VeriComp

- Behaviour
- Well_founded
- Inf
- Transfer_Extras
- Semantics
- Language
- Simulation
- Compiler
- Fixpoint

### Used by

- Inline Caching and Unboxing Optimization for Interpreters

## Cite

×

VeriComp-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Feb 25, 2020 : Isabelle2019