Inline Caching and Unboxing Optimization for Interpreters

 

Title: Inline Caching and Unboxing Optimization for Interpreters
Author: Martin Desharnais
Submission date: 2020-12-07
Abstract: This Isabelle/HOL formalization builds on the VeriComp entry of the Archive of Formal Proofs to provide the following contributions:
  • an operational semantics for a realistic virtual machine (Std) for dynamically typed programming languages;
  • the formalization of an inline caching optimization (Inca), a proof of bisimulation with (Std), and a compilation function;
  • the formalization of an unboxing optimization (Ubx), a proof of bisimulation with (Inca), and a simple compilation function.
This formalization was described in the CPP 2021 paper Towards Efficient and Verified Virtual Machines for Dynamic Languages
BibTeX:
@article{Interpreter_Optimizations-AFP,
  author  = {Martin Desharnais},
  title   = {Inline Caching and Unboxing Optimization for Interpreters},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2020,
  note    = {\url{https://isa-afp.org/entries/Interpreter_Optimizations.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: VeriComp