https://martin.desharnais.me
This is an unofficial reimagining of the Archive of Formal Proofs
Inline Caching and Unboxing Optimization for Interpretersby Martin Desharnais
A Generic Framework for Verified Compilersby Martin Desharnais