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

### License

BSD License

### History

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

### Topics

- Computer science/Programming languages/Misc

### Session Interpreter_Optimizations

- Env
- Env_list
- List_util
- Result
- Option_Extra
- Map_Extra
- AList_Extra
- Global
- Op
- OpInl
- Dynamic
- Inca
- Unboxed
- OpUbx
- Ubx
- Ubx_Verification
- Unboxed_lemmas
- Inca_to_Ubx_simulation
- Inca_Verification
- Inca_to_Ubx_compiler
- Op_example
- Std
- Std_to_Inca_simulation
- Std_to_Inca_compiler

### Depends on

- A Generic Framework for Verified Compilers

## Cite

×

Interpreter_Optimizations-AFP

    @article{Interpreter_Optimizations-AFP,
      author  = {Martin Desharnais},
      title   = {Inline Caching and Unboxing Optimization for Interpreters},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Interpreter_Optimizations.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021