A Generic Framework for Verified Compilers (Q7361691)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry VeriComp
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Generic Framework for Verified Compilers |
AFP entry VeriComp |
Statements
10 February 2020
0 references
Martin Desharnais-Schäfer
0 references
A Generic Framework for Verified Compilers (English)
0 references
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.
0 references
