Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A Generic Framework for Verifi...

Email Gateway (Aug 23 2022 at 08:19):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
A Generic Framework for Verified Compilers
by Martin Desharnais

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.

Available at https://www.isa-afp.org/entries/VeriComp.html

Enjoy,
René

Last updated: Apr 26 2024 at 20:16 UTC