Inline Caching and Unboxing Optimization for Interpreters

Martin Desharnais 🌐

December 7, 2020


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


BSD License


June 25, 2021
proved conditional completeness of compilation
June 14, 2021
refactored function definitions to contain explicit basic blocks


Session Interpreter_Optimizations