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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.