Inline Caching and Unboxing Optimization for Interpreters (Q7361287)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Interpreter_Optimizations
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Inline Caching and Unboxing Optimization for Interpreters |
AFP entry Interpreter_Optimizations |
Statements
7 December 2020
0 references
Martin Desharnais-Schäfer
0 references
Inline Caching and Unboxing Optimization for Interpreters (English)
0 references
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
0 references
