Inline Caching and Unboxing Optimization for Interpreters

Martin Desharnais

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

Change history

[2021-06-14] refactored function definitions to contain explicit basic blocks
[2021-06-25] proved conditional completeness of compilation

Depends On