Certifying Compilation for a Language with Stack Allocation. - Limin Jia 001; Frances Spalding; David Walker 001; Neal Glew (LICS, 2005)