solidity中的SMT（1）
Solidity实现了一种基于SMT（Satisfiability Modulo Theories）和Horn逻辑的形式化验证方法。
Runtime feedback in a meta-tracing JIT for efficient dynamic languages
ECOOP2011，meta-tracing jit通过运行时信息优化object model，核心在于promotion实现的constant fold和operation fold，以及它们的结合体。
The Impact of Meta-Tracing on VM Design and Implementation
来自SCP2015，相对详细说明了PyPy JIT优化的一些设计。不过缺少Runtime信息的辅助，留到Runtime feedback in a meta-tracing那篇。
Tracing the meta-level:\ PyPy's tracing JIT compiler
ECOOP09，PyPy JIT设计的第一篇，某种意义上算是meta-tracing的开山之作！？（大概，不是很确定）
Rethinking Incremental and Parallel Pointer Analysis
Rethinking Incremental and Parallel Pointer Analysis来自TOPLAS，介绍了一种增量的可并行的指针分析算法。
Lazy Basic Block Versioning续
Interprocedural Type Specialization of JavaScript Programs Without Type Analysis 来自ECOOP2016，是在Simple and Effective Type Check Removal through Lazy Basic Block Versioning基础上实现的，主要将BBV扩展到interprocedura
Lazy Basic Block Versioning
Simple and Effective Type Check Removal through Lazy Basic Block Versioning，这篇论文来自ECOOP2015，介绍了一种可以有效消除类型检查的技术，用于动态类型语言的JIT编译。
Functional programming compiler optimization
Can a functional programming language compiler optimize as well as an imperative programming language compiler in practice?在搜索FP优化的时候看到这么一个问题